Este é o comando lpsconfcheck que pode ser executado no provedor de hospedagem gratuita OnWorks usando uma de nossas várias estações de trabalho online gratuitas, como Ubuntu Online, Fedora Online, emulador online do Windows ou emulador online do MAC OS
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