ltsconvert - Online na nuvem

PROGRAMA:

NOME

ltsconvert - converte e, opcionalmente, minimiza um LTS

SINOPSE

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

DESCRIÇÃO

Converta o sistema de transição rotulado (LTS) de INFILE para OUTFILE no pedido
depois de aplicar o método de minimização selecionado (o padrão é nenhum). Se OUTFILE for
não fornecido, stdout é usado. Se INFILE não for fornecido, stdin será usado.

O formato de saída é determinado pela extensão de OUTFILE, enquanto o formato de entrada é
determinado pelo conteúdo do INFILE. As opções --in e --out podem ser usadas para forçar a entrada
e formatos de saída. 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 (padrão)

OPÇÕES

OPÇÃO pode ser qualquer um dos seguintes:

-D, --determinar
determinar LTS

-eNOME, --equivalência=NOME
gerar um LTS equivalente, preservando a equivalência NOME: identidade 'nenhuma'
equivalência (padrão) 'bisim' bissimilaridade forte 'bisim-sig' bissimilaridade forte
usando refinamento de assinatura 'branching-bisim' branching bisimilarity 'branching-
bisim-sig 'bissimilaridade de ramificação usando refinamento de assinatura' dpbranching-bisim '
divergência preservando ramificação bissimilaridade 'dpbranching-bisim-sig' divergência
preservando bissimilaridade de ramificação usando refinamento de assinatura 'bisim fraco' fraco
bisimilaridade 'fraco-bisim-sig' bissimilaridade fraca usando refinamento de assinatura 'dpweak-
divergência bisim 'preservando bisimilaridade fraca' dpweak-bisim-sig 'divergência
preservando a bissimilaridade fraca usando simulação forte de refinamento de assinatura 'sim'
equivalência 'traço' equivalência de traço forte 'traço fraco' equivalência de traço fraco
'tau-star' redução da estrela tau

-iFORMATO, --no=FORMATO
use FORMAT como formato de entrada

-lARQUIVO, --lps=ARQUIVO
use FILE como o LPS a partir do qual o LTS de entrada foi gerado; isso pode ser necessário para
armazene os nomes dos parâmetros corretos dos estados ao salvar no formato fsm e para
converter não-mCRL2 LTSs em mCRL2 LTS

- sem alcance
não execute uma verificação de acessibilidade no LTS de entrada

-n, --sem estado
omita informações de estado ao salvar em formato de ponto

-oFORMATO, --Fora=FORMATO
use FORMAT como formato de saída

--tau=NOMES DE ATO
considere as ações com um nome na lista separada por vírgulas ACTNAMES como internas
(tau) ações além daquelas definidas como tal pela entrada

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

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 ltsconvert online usando serviços onworks.net