EnglishFrenchSpanish

Ad


OnWorks favicon

lps2lts - Online in the Cloud

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

This is the command lps2lts 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


lps2lts - generate an LTS from an LPS

SYNOPSIS


lps2lts [OPTION]... [INFILE [OUTFILE]]

DESCRIPTION


Generate an LTS from the LPS in INFILE and save the result to OUTFILE. If INFILE is not
supplied, stdin is used. If OUTFILE is not supplied, the LTS is not stored.

If the 'jittyc' rewriter is used, then the MCRL2_COMPILEREWRITER environment variable
(default value: 'mcrl2compilerewriter') determines the script that compiles the rewriter,
and MCRL2_COMPILEDIR (default value: '.') determines where temporary files are stored.

Note that lps2lts can deliver multiple transitions with the same label betweenany pair of
states. If this is not desired, such transitions can be removed byapplying a strong
bisimulation reducton using for instance the tool ltsconvert.

The format of OUTFILE is determined by its extension (unless it is specified by an
option). The supported formats are:

'aut' for the Aldebaran format (CADP),
'dot' for the GraphViz format (no longer supported as input format),
'fsm' for the Finite State Machine format, or
'lts' for the mCRL2 LTS format If the jittyc rewriter is used, then the
MCRL2_COMPILEREWRITER environment variable (default value: mcrl2compilerewriter)
determines the script that compiles the rewriter, and MCRL2_COMPILEDIR (default value:
'.') determines where temporary files are stored. Note that lps2lts can deliver multiple
transitions with the same label between any pair of states. If this is not desired, such
transitions can be removed by applying a strong bisimulation reducton using for instance
the tool ltsconvert.

OPTIONS


OPTION can be any of the following:

-aNAMES, --action=NAMES
detect and report actions in the transitions system that have action names from
NAMES, a comma-separated list. This is for instance useful to find (or prove the
absence) of an action error. A message is printed for every occurrence of one of
these action names. With the -t flag traces towards these actions are generated

-b[NUM], --bit-hash[=NUM]
use bit hashing to store states and store at most NUM states. This means that
instead of keeping a full record of all states that have been visited, a bit array
is used that indicate whether or not a hash of a state has been seen before.
Although this means that this option may cause states to be mistaken for others
(because they are mapped to the same hash), it can be useful to explore very large
LTSs that are otherwise not explorable. The default value for NUM is approximately
2*10^8 (this corresponds to about 25MB of memory)

--cached
use enumeration caching techniques to speed up state space generation.

-c[NAME], --confluence[=NAME]
apply prioritization of transitions with the action label NAME.(when no NAME is
supplied (i.e., '-c') priority is given to the action 'ctau'. To give priority to
to tau use the flag -ctau. Note that if the linear process is not tau-confluent,
the generated state space is necessarily branching bisimilar to the state space of
the lps. The generation algorithm that is used does not require the linear process
to be tau convergent.

-D, --deadlock
detect deadlocks (i.e. for every deadlock a message is printed)

-F, --divergence
detect divergences (i.e. for every state with a divergence (=tau loop) a message is
printed). The algorithm to detect the divergences is linear for every state, so
state space exploration becomes quadratic with this option on, causing a state
space exploration to become slow when this option is enabled.

-yBOOL, --dummy=BOOL
replace free variables in the LPS with dummy values based on the value of BOOL:
'yes' (default) or 'no'

--error-trace
if an error occurs during exploration, save a trace to the state that could not be
explored

--init-tsize=NUM
set the initial size of the internally used hash tables (default is 10000)

-lNUM, --max=NUM
explore at most NUM states

-mNAMES, --multiaction=NAMES
detect and report multiactions in the transitions system from NAMES, a comma-
separated list. Works like -a, except that multi-actions are matched exactly,
including data parameters.

--no-info
do not add state information to OUTFILEWithout this option lps2lts adds state
vector to the LTS. This option causes this information to be discarded and states
are only indicated by a sequence number. Explicit state information is useful for
visualisation purposes, for instance, but can cause the OUTFILE to grow
considerably. Note that this option is implicit when writing in the AUT format.

-oFORMAT, --out=FORMAT
save the output in the specified FORMAT

--prune
use summand pruning to speed up state space generation.

-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

-sNAME, --strategy=NAME
explore the state space using strategy NAME: 'b', 'breadth' breadth-first search
(default) 'd', 'depth' depth-first search 'p', 'prioritized' prioritize single
actions on its first argument being of sort Nat where only those actions with the
lowest value for this parameter are selected. E.g. if there are actions a(3) and
b(4), a(3) remains and b(4) is skipped. Actions without a first parameter of sort
Nat and multactions with more than one action are always chosen (option is
experimental) 'q', 'rprioritized' prioritize actions on its first argument being of
sort Nat (see option --prioritized), and randomly select one of these to obtain a
prioritized random simulation (option is experimental) 'r', 'random' random
simulation. Out of all next states one is chosen at random independently of whether
this state has already been observed. Consequently, random simultation only
terminates when a deadlocked state is encountered.

--suppress
in verbose mode, do not print progress messages indicating the number of visited
states and transitions. For large state spaces the number of progress messages can
be quite horrendous. This feature helps to suppress those. Other verbose messages,
such as the total number of states explored, just remain visible.

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

--todo-max=NUM
keep at most NUM states in todo lists; this option is only relevant for breadth-
first search, where NUM is the maximum number of states per level, and for depth
first search, where NUM is the maximum depth

-t[NUM], --trace[=NUM]
Write a shortest trace to each state that is reached with an action from NAMES from
option --action, is a deadlock detected with --deadlock, or is a divergence
detected with --divergence to a file. No more than NUM traces will be written. If
NUM is not supplied the number of traces is unbounded.For each trace that is to be
written a unique file with extension .trc (trace) will be created containing a
shortest trace from the initial state to the deadlock state. The traces can be
pretty printed and converted to other formats using tracepp.

-u, --unused-data
do not remove unused parts of the data specification

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 lps2lts online using onworks.net services


Free Servers & Workstations

Download Windows & Linux apps

  • 1
    DivFix++
    DivFix++
    DivFix++ is yours AVI video repair and
    preview software. It designed for repair
    and preview files which are on download
    from ed2k(emule), torrent, gnutella, ftp...
    Download DivFix++
  • 2
    JBoss Community
    JBoss Community
    Community driven projects featuring the
    latest innovations for cutting edge
    apps. Our flagship project JBoss AS is
    the leading Open Source,
    standards-compliant...
    Download JBoss Community
  • 3
    Django Filer
    Django Filer
    django Filer is a file management
    application for django that makes
    handling files and images a breeze.
    django-filer is a file management
    application for djang...
    Download Django Filer
  • 4
    xCAT
    xCAT
    Extreme Cluster Administration Toolkit.
    xCAT is a scalable cluster management
    and provisioning tool that provides
    hardware control, discovery, and OS
    diskful/di...
    Download xCAT
  • 5
    Psi
    Psi
    Psi is cross-platform powerful XMPP
    client designed for experienced users.
    There are builds available for MS
    Windows, GNU/Linux and macOS.. Audience:
    End Users...
    Download Psi
  • 6
    Blobby Volley 2
    Blobby Volley 2
    Official continuation of the famous
    Blobby Volley 1.x arcade game..
    Audience: End Users/Desktop. User
    interface: OpenGL, SDL. Programming
    Language: C++, Lua. C...
    Download Blobby Volley 2
  • More »

Linux commands

Ad