lpsrealelm
The tool replaces parameters of sort real from the linear process specification
by parameters of sort Comp
, which is an structured sort with three constants
smaller
, equal
and larger
. They represent that certain pairs of real
expressions must be smaller, equal or larger to each other. If the resulting
linear process does not contain MAY
-actions, it is strongly bisimilar to the
input lps. Otherwise, the result is may-bisimilar to the original.
Example
Consider an LPS with the following process equation.
act step, urgent, reset;
proc P(x:Real) = sum y:Real.(x<y)->step.P(y)
+ sum y:Real.(x<y && x<2)->urgent.P(y)
+ reset.P(0);
init P(0);
The tool transforms this to the following strongly bisimilar LPS
(where it must be noted that in this particular case the condition
x>=0
has been added to each summand in the input LPS).
sort Comp = struct smaller?is_smaller | equal?is_equal | larger?is_larger;
act step,urgent,reset;
proc P(xi,xi00: Comp) =
!is_smaller(xi) ->
reset .
P(equal, smaller)
+ (is_smaller(xi00) && !is_smaller(xi)) ->
urgent .
P(larger, equal)
+ (!is_smaller(xi) && is_smaller(xi00)) ->
urgent .
P(larger, smaller)
+ (is_smaller(xi00) && !is_smaller(xi)) ->
urgent .
P(larger, larger)
+ (is_smaller(xi00) && !is_smaller(xi)) ->
step .
P(larger, equal)
+ (!is_smaller(xi) && is_smaller(xi00)) ->
step .
P(larger, smaller)
+ !is_smaller(xi) ->
step .
P(larger, larger);
init P(equal, smaller);
- orphan:
Usage
lpsrealelm [OPTION]... [INFILE [OUTFILE]]
Description
Remove Real numbers from the linear process specification (LPS) in INFILE and write the result to OUTFILE. If INFILE is not present, stdin is used.
Command line options
--max=NUM
perform at most NUM iterations
-QNUM
, --qlimit=NUM
limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).
-rNAME
, --rewriter=NAME
use rewrite strategy NAME:
jitty
jitty rewriting
jittyc
compiled jitty rewriting
jittyp
jitty rewriting with prover
--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 log messages
-d
, --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h
, --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options