lpsconfcheck - Online na nuvem

PROGRAMA:

NOME

lpsconfcheck - marca tau-summands confluentes de um LPS

SINOPSE

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

DESCRIÇÃO

Verifica quais tau-summands do mCRL2 LPS em INFILE são confluentes, marca-os renomeando
-los em ctau e escrever o resultado em OUTFILE. Se INFILE não estiver presente, stdin é usado. Se
OUTFILE não está presente, stdout é usado.

OPÇÕES

OPÇÃO pode ser qualquer um dos seguintes:

-a, - verificar tudo
verifique a confluência de tau-summands em relação a todos os outros summands, em vez de
continuando com o próximo tau-summand assim que for encontrado um summand que seja
não confluente com o tau-summand atual

-c, --contra-exemplo
exibir uma avaliação para a qual a condição de confluência não se aplica, no caso de
condição encontrada não é uma contradição nem uma tautologia

-g, --gerar-invariantes
tentar provar que a condição de confluência reduzida é invariante do LPS, em
caso a condição de confluência não seja uma tautologia

-o, --indução
aplicar indução em listas

-iINVFILE, --invariante=INVFILE
use a fórmula booleana (uma expressão de dados mCRL2 do tipo Bool) em INVFILE como
invariante

-n, - não verificar
não verifique se o invariante se mantém antes de verificar a confluência

-m, - sem marcação
não marque os tau-summands confluentes; uma vez que não há alterações feitas no LPS,
nada é escrito em OUTFILE

-pPREFIXO, --print-ponto=PREFIXO
salve um arquivo .dot do BDD resultante, caso dois summands não possam ser comprovados
confluente; PREFIX será usado como prefixo dos arquivos de saída

-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

-zSOLUCIONADOR, --smt-solucionador=SOLUCIONADOR
use o SOLVER para remover caminhos inconsistentes dos BDDs usados ​​internamente (por padrão,
nenhuma eliminação de caminho é aplicada): 'cvc' o solucionador SMT CVC3

-sNUM, --parcela=NUM
elimine ou simplifique a soma apenas com o número NUM

-tLIMITE, --limite de tempo=LIMITE
gaste no máximo LIMIT segundos para provar uma única fórmula

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