lps2lts - Online na nuvem

PROGRAMA:

NOME

lps2lts - gera um LTS a partir de um LPS

SINOPSE

lps2lts [OPÇÃO] ... [NO ARQUIVO [ARQUIVO]]

DESCRIÇÃO

Gere um LTS do LPS em INFILE e salve o resultado em OUTFILE. Se INFILE não for
fornecido, stdin é usado. Se OUTFILE não for fornecido, o LTS não será armazenado.

Se o reescritor 'jittyc' for usado, então a variável de ambiente MCRL2_COMPILEREWRITER
(valor padrão: 'mcrl2compilerewriter') determina o script que compila o reescritor,
e MCRL2_COMPILEDIR (valor padrão: '.') determina onde os arquivos temporários são armazenados.

Observe que lps2lts pode fornecer várias transições com o mesmo rótulo entre qualquer par de
estados. Se isso não for desejado, tais transições podem ser removidas aplicando um forte
redução de bisimulação usando, por exemplo, a ferramenta ltsconvert.

O formato de OUTFILE é determinado por sua extensão (a menos que seja especificado por um
opção). Os formatos suportados são:

'aut' para o formato Aldebaran (CADP),
'ponto' para o formato GraphViz (não é mais suportado como formato de entrada),
'fsm' para o formato Finite State Machine, ou
'lts' para o formato mCRL2 LTS Se o jittyc rewriter for usado, então o
Variável de ambiente MCRL2_COMPILEREWRITER (valor padrão: mcrl2compilerewriter)
determina o script que compila o reescritor e MCRL2_COMPILEDIR (valor padrão:
'.') determina onde os arquivos temporários são armazenados. Observe que lps2lts pode fornecer vários
transições com o mesmo rótulo entre qualquer par de estados. Se isso não for desejado, tal
as transições podem ser removidas aplicando uma forte redução de bissimulação usando, por exemplo
a ferramenta ltsconvert.

OPÇÕES

OPÇÃO pode ser qualquer um dos seguintes:

-aNOMES, --açao=NOMES
detectar e relatar ações no sistema de transições que têm nomes de ação de
NAMES, uma lista separada por vírgulas. Isso é útil, por exemplo, para encontrar (ou provar o
ausência) de um erro de ação. Uma mensagem é impressa para cada ocorrência de um dos
esses nomes de ação. Com o sinalizador -t, traços para essas ações são gerados

-b[NUM], --bit-hash[=NUM]
use hashing de bits para armazenar estados e armazenar no máximo NUM estados. Isso significa que
em vez de manter um registro completo de todos os estados que foram visitados, uma matriz de bits
é usado para indicar se um hash de um estado foi visto antes ou não.
Embora isso signifique que esta opção pode fazer com que os estados sejam confundidos com outros
(porque eles são mapeados para o mesmo hash), pode ser útil explorar grandes
LTSs que de outra forma não são exploráveis. O valor padrão para NUM é aproximadamente
2 * 10 ^ 8 (isso corresponde a cerca de 25 MB de memória)

- em cache
use técnicas de cache de enumeração para acelerar a geração de espaço de estado.

-c[NOME], --confluência[=NOME]
aplique a priorização de transições com o rótulo de ação NAME. (quando nenhum NAME é
a prioridade fornecida (isto é, '-c') é dada à ação 'ctau'. Para dar prioridade a
para tau use a sinalização -ctau. Observe que se o processo linear não for tau-confluente,
o espaço de estado gerado é necessariamente bissimilar ao espaço de estado de
o lps. O algoritmo de geração que é usado não requer o processo linear
para ser tau convergente.

-D, --impasse
detectar deadlocks (ou seja, para cada deadlock uma mensagem é impressa)

-F, --divergência
detectar divergências (ou seja, para cada estado com uma divergência (= loop tau), uma mensagem é
impresso). O algoritmo para detectar as divergências é linear para cada estado, então
a exploração do espaço de estado torna-se quadrática com esta opção ativada, causando um estado
a exploração do espaço torna-se lenta quando esta opção é ativada.

-yBOOL, --fictício=BOOL
substitua as variáveis ​​livres no LPS por valores fictícios com base no valor de BOOL:
'sim' (padrão) ou 'não'

--rastreamento de erro
se ocorrer um erro durante a exploração, salve um traço para o estado que não poderia ser
explorados

--init-tsize=NUM
definir o tamanho inicial das tabelas de hash usadas internamente (o padrão é 10000)

-lNUM, --máx.=NUM
explore no máximo NUM estados

-mNOMES, --multiação=NOMES
detectar e relatar multiações no sistema de transições de NAMES, uma vírgula
lista separada. Funciona como -a, exceto que as múltiplas ações são correspondidas exatamente,
incluindo parâmetros de dados.

--Nenhuma informação
não adicione informações de estado a OUTFILE; sem esta opção lps2lts adiciona estado
vetor para o LTS. Esta opção faz com que esta informação seja descartada e estados
são indicados apenas por um número de sequência. Informações explícitas sobre o estado são úteis para
fins de visualização, por exemplo, mas pode fazer com que OUTFILE cresça
consideravelmente. Observe que esta opção está implícita ao gravar no formato AUT.

-oFORMATO, --Fora=FORMATO
salvar a saída no FORMATO especificado

--ameixa seca
use sumar poda para acelerar a geração de espaço de estado.

-QNUM, --qlimit=NUM
limite a enumeração de quantificadores a variáveis ​​NUM. (Padrão NUM = 1000, NUM = 0 para
ilimitado).

-rNOME, --reescritor=NOME
usar estratégia de reescrita NOME: 'jitty' jitty reescrita (padrão) 'jittyc' compilado
jitty reescrevendo 'jittyp' jitty reescrevendo com provador

-sNOME, --estratégia=NOME
explore o espaço de estado usando a estratégia NOME: 'b', 'amplitude' pesquisa em largura primeiro
(padrão) 'd', 'profundidade' pesquisa em profundidade 'p', 'priorizado' priorizar único
ações em seu primeiro argumento sendo do tipo Nat, onde apenas as ações com o
o valor mais baixo para este parâmetro são selecionados. Por exemplo, se houver ações a(3) e
b(4) a(3) permanece e b(4) é ignorado. Ações sem um primeiro parâmetro de classificação
Nat e multações com mais de uma ação são sempre escolhidos (a opção é
experimental) 'q', 'priorizado' priorizam ações em seu primeiro argumento sendo de
classificar Nat (ver opção --prioritized), e selecionar aleatoriamente um deles para obter um
simulação aleatória priorizada (a opção é experimental) 'r', 'aleatório' aleatório
simulação. De todos os próximos estados, um é escolhido aleatoriamente, independentemente de
este estado já foi observado. Consequentemente, apenas a simultaneidade aleatória
termina quando um estado de deadlock é encontrado.

--suprimir
no modo detalhado, não imprime mensagens de progresso indicando o número de visitantes
estados e transições. Para grandes espaços de estado, o número de mensagens de progresso pode
ser horrível. Este recurso ajuda a suprimir aqueles. Outras mensagens verbosas,
como o número total de estados explorados, apenas permanecem visíveis.

--tempos[=ARQUIVO]
anexar medições de tempo a ARQUIVO. As medições são gravadas no erro padrão se
nenhum FILE é fornecido

--todo-max=NUM
manter no máximo NUM estados em listas de tarefas; esta opção é relevante apenas para amplitude-
primeira pesquisa, onde NUM é o número máximo de estados por nível e para profundidade
primeira pesquisa, onde NUM é a profundidade máxima

-t[NUM], --vestígio[=NUM]
Escreva um traço mais curto para cada estado alcançado com uma ação de NAMES de
opção --action, é um deadlock detectado com --deadlock, ou é uma divergência
detectado com --divergence para um arquivo. Não mais do que NUM traços serão gravados. Se
NUM não é fornecido, o número de rastreios é ilimitado. Para cada rastreio que deve ser
escrito, um arquivo único com extensão .trc (trace) será criado contendo um
menor rastreio do estado inicial ao estado de conflito. Os rastros podem ser
muito impresso e convertido para outros formatos usando tracepp.

-u, --dados não usados
não remova partes não utilizadas da especificação de dados

Opções padrão:

-q, --quieto
não exibir mensagens de aviso

-v, --verbose
exibir mensagens intermediárias curtas

-d, --depurar
exibir mensagens intermediárias detalhadas

--log-level=NÍVEL
exibir mensagens intermediárias até e incluindo o nível

-h, --Socorro
exibir informações de ajuda

--versão
exibir informações da versão

Use lps2lts online usando serviços onworks.net