EnglishFrenchSpanish

Ad


OnWorks favicon

lpsinvelm - Online in the Cloud

Run lpsinvelm in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

This is the command lpsinvelm that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

PROGRAM:

NAME


lpsinvelm - check invariants and use these to simplify or eliminate summands of an LPS

SYNOPSIS


lpsinvelm [OPTION]... --invfile=INVFILE [INFILE [OUTFILE]]

DESCRIPTION


Checks whether the boolean formula (an mCRL2 data expression of sort Bool) provided as
invariant is an invariant of the linear process specification (LPS) in INFILE. If this is
the case, the tool eliminates all summands of the LPS whose condition violates the
invariant, and writes the result to OUTFILE. If INFILE is present, stdin is used. If
OUTFILE is not present, stdout is used.

The tool can also be used to simplify the conditions of the summands of the given LPS.

OPTIONS


OPTION can be any of the following:

-y, --all-violations
do not terminate as soon as a single violation of the invariant is found, but
report all violations instead

-c, --counter-example
display a valuation indicating why the invariant could possibly be violated if it
is uncertain whether a summand violates the invariant

-o, --induction
apply induction on lists

-iINVFILE, --invariant=INVFILE
use the boolean formula (an mCRL2 data expression of sort Bool) in INVFILE as
invariant

-n, --no-check
do not check if the invariant holds before eliminating unreachable summands

-e, --no-elimination
do not eliminate or simplify summands, but add the invariant to each condition

-pPREFIX, --print-dot=PREFIX
save a .dot file of the resulting BDD if it is impossible to determine whether a
summand violates the invariant; PREFIX will be used as prefix of the output files

-QNUM, --qlimit=NUM
limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for
unlimited).

-rNAME, --rewriter=NAME
use rewrite strategy NAME: 'jitty' jitty rewriting (default) 'jittyc' compiled
jitty rewriting 'jittyp' jitty rewriting with prover

-l, --simplify-all
simplify the conditions of all summands, instead of just eliminating the summands
whose conditions in conjunction with the invariant are contradictions

-zSOLVER, --smt-solver=SOLVER
use SOLVER to remove inconsistent paths from the internally used BDDs (by default,
no path elimination is applied): 'cvc' the SMT solver CVC3

-tLIMIT, --time-limit=LIMIT
spend at most LIMIT seconds on proving a single formula

--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if
no FILE is provided

Standard options:

-q, --quiet
do not display warning messages

-v, --verbose
display short intermediate messages

-d, --debug
display detailed intermediate messages

--log-level=LEVEL
display intermediate messages up to and including level

-h, --help
display help information

--version
display version information

Use lpsinvelm online using onworks.net services


Free Servers & Workstations

Download Windows & Linux apps

  • 1
    AstrOrzPlayer
    AstrOrzPlayer
    AstrOrz Player is a free media player
    software, part based on WMP and VLC. The
    player is in a minimalist style, with
    more than ten theme colors, and can also
    b...
    Download AstrOrzPlayer
  • 2
    movistartv
    movistartv
    Kodi Movistar+ TV es un ADDON para XBMC/
    Kodi que permite disponer de un
    decodificador de los servicios IPTV de
    Movistar integrado en uno de los
    mediacenters ma...
    Download movistartv
  • 3
    Code::Blocks
    Code::Blocks
    Code::Blocks is a free, open-source,
    cross-platform C, C++ and Fortran IDE
    built to meet the most demanding needs
    of its users. It is designed to be very
    extens...
    Download Code::Blocks
  • 4
    Amidst
    Amidst
    Amidst or Advanced Minecraft Interface
    and Data/Structure Tracking is a tool to
    display an overview of a Minecraft
    world, without actually creating it. It
    can ...
    Download Amidst
  • 5
    MSYS2
    MSYS2
    MSYS2 is a collection of tools and
    libraries providing you with an
    easy-to-use environment for building,
    installing and running native Windows
    software. It con...
    Download MSYS2
  • 6
    libjpeg-turbo
    libjpeg-turbo
    libjpeg-turbo is a JPEG image codec
    that uses SIMD instructions (MMX, SSE2,
    NEON, AltiVec) to accelerate baseline
    JPEG compression and decompression on
    x86, x8...
    Download libjpeg-turbo
  • More »

Linux commands

  • 1
    abi-tracker
    abi-tracker
    abi-tracker - visualize ABI changes
    timeline of a C/C++ software library.
    DESCRIPTION: NAME: ABI Tracker
    (abi-tracker) Visualize ABI changes
    timeline of a C/C+...
    Run abi-tracker
  • 2
    abicheck
    abicheck
    abicheck - check application binaries
    for calls to private or evolving symbols
    in libraries and for static linking of
    some system libraries. ...
    Run abicheck
  • 3
    couriermlm
    couriermlm
    couriermlm - The Courier mailing list
    manager ...
    Run couriermlm
  • 4
    couriertcpd
    couriertcpd
    couriertcpd - the Courier mail server
    TCP server daemon ...
    Run couriertcpd
  • 5
    gbklatex
    gbklatex
    bg5latex - Use LaTeX directly on a Big5
    encodedtex file bg5pdflatex - Use
    pdfLaTeX directly on a Big5 encodedtex
    file bg5+latex - Use LaTeX directly on a
    Big5+...
    Run gbklatex
  • 6
    gbkpdflatex
    gbkpdflatex
    bg5latex - Use LaTeX directly on a Big5
    encodedtex file bg5pdflatex - Use
    pdfLaTeX directly on a Big5 encodedtex
    file bg5+latex - Use LaTeX directly on a
    Big5+...
    Run gbkpdflatex
  • More »

Ad