lpsinvelm - Online na nuvem

PROGRAMA:

NOME

lpsinvelm - verifica as invariantes e usa-as para simplificar ou eliminar summands de um LPS

SINOPSE

lpsinvelm [OPÇÃO] ... --invfile = INVFILE [NO ARQUIVO [ARQUIVO]]

DESCRIÇÃO

Verifica se a fórmula booleana (uma expressão de dados mCRL2 do tipo Bool) fornecida como
invariante é um invariante da especificação do processo linear (LPS) em INFILE. Se isso é
caso, a ferramenta elimina todos os summands do LPS cuja condição viola o
invariante e grava o resultado em OUTFILE. Se INFILE estiver presente, stdin será usado. Se
OUTFILE não está presente, stdout é usado.

A ferramenta também pode ser usada para simplificar as condições dos somatórios do LPS fornecido.

OPÇÕES

OPÇÃO pode ser qualquer um dos seguintes:

-y, --todas as violações
não termine assim que uma única violação do invariante for encontrada, mas
relatar todas as violações em vez disso

-c, --contra-exemplo
exibir uma avaliação indicando porque o invariante poderia ser violado se
é incerto se um summand viola o invariante

-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 eliminar somandos inalcançáveis

-e, --não-eliminação
não elimina ou simplifica somas, mas adiciona o invariante a cada condição

-pPREFIXO, --print-ponto=PREFIXO
salve um arquivo .dot do BDD resultante se for impossível determinar se um
summand viola o invariante; 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

-l, - simplificar tudo
simplificar as condições de todos os summands, em vez de apenas eliminar os summands
cujas condições em conjunto com o invariante são contradições

-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

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