# 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

### Author

Jan Friso Groote and Jeroen Keiren