The lpsactionrename
tool renames actions in an LPS, based on their names and
on the data parameters they carry. The tool can be used in two ways: either by
supplying it with a rename file or by providing a regular expression. A rename
file is provided using the option --renamefile
and a regular expression can
be specified with the option --regex
. Both modes are explained below.
ActionRenameRuleRHS ActionRenameRule ActionRenameRuleSpec ActionRenameSpec
ActionRenameRuleRHS ::=Action
| 'tau' | 'delta' ActionRenameRule ::= (DataExpr
'->' ) ?Action
'=>'ActionRenameRuleRHS
';' ActionRenameRuleSpec ::=VarSpec
? 'rename'ActionRenameRule
+ ActionRenameSpec ::= (SortSpec
|ConsSpec
|MapSpec
|EqnSpec
|ActSpec
|ActionRenameRuleSpec
) +
The format of the RENAMEFILE can contain sort
, cons
, map
, eqn
and act
sections as in a mcrl2 file. This is followed by a rename
section to define the rename rules. The sections sort
, cons
, map
,
eqn
and act
are meant for new declarations that will be added to the LPS
and can be used in the rename rules. The new declarations are not allowed to
contain any conflicts with the declarations of the LPS. The rename
section
can be preceded by a var
section, where variables can be declared for the
rename rules.
The rename rules have the format: rename c -> a1 => a2;
where c
is a
boolean expression that has to hold to rename an occurrence of a1
into
a2
. The condition can be left out, in which case it is interpreted as
true
(i.e., all occurrences of a1
will be renamed). The action a1
can contain arguments that can either be uniquely occurring variables or closed
terms. The arguments of a2
can be arbitrary terms, but the variables
occurring in it must also occur in a1
. The condition is an expression of
sort Bool
and can also only use variables that also occur in a1
.
It is possible use tau
for a2
; note that this means that a
multi-action of the form a1|b
will be replaced by b
. Instead of an
action, a2
may also be delta
. In this case, the action and the following
process call are replaced by delta
.
The renaming rules are applied from top to bottom to a linear process equation. If no value for the variables in a rename rule can be found to match an action, the next rule is applied. If no rule applies the action is left untouched. Variables in different rename rules with the same variable names are independent when being matched.
After the LPS has been renamed, sum elimination and rewriting will be applied to simplify the result. This can be skipped using appropriate switches.
Upon loading the rename file, lpsactionrename
will check if the following
conditions hold:
Bool
.Consider an LPS with the process specification:
P(x:Bool) = sum y:Nat. (y < 6) -> a(x,y). P(!x);
and a rename file with the following rename rules:
act b: Bool;
var v: Nat; w:Bool;
rename
w -> a(w,v) => b(v==5);
(v==v*2)==w -> a(w,v) => tau;
a(w,5) => delta;
The arguments of an action do not have to consist of a single variable, as is
done in the second rename rule. In the second rename rule, a(w,2*v)
, w
and 2*v
will be respectively equal to x
and y
from the LPS action
a(x,y)
.
The result of applying the rename rules to the LPS without sum elimination will give:
proc P(x_P0: Bool) =
true ->
delta
+ sum w: Bool,v,y_P0: Nat.
((y_P0 < 6 && w==x_P0 && v==y_P0) && w) -> b(v==5).P(!x_P0);
+ sum w00: Bool,v00: Nat,w: Bool,v,y_P0: Nat.
((((y_P0 < 6 && w==x_P0 && v==y_P0) && !w) && w00==x_P0 && v00==y_P0) &&
(v00==v00*2)==w00) -> tau.P(!x_P0)
+ sum w01,w00: Bool,v00: Nat,w: Bool,v,y_P0: Nat.
((((((y_P0 < 6 && w==x_P0 && v==y_P0) && !w) && w00==x_P0 && v00==y_P0) &&
!((v00==v00*2)==w00)) && w01==x_P0) && 5==y_P0) -> delta
+ sum w01,w00: Bool,v00: Nat,w: Bool,v,y_P0: Nat.
((((((y_P0 < 6 && w==x_P0 && v==y_P0) && !w) && w00==x_P0 && v00==y_P0) &&
!((v00==v00*2)==w00)) && w01==x_P0) && !(5==y_P0)) -> a(x_P0, y_P0).P(!x_P0)
Most of the introduced sum variables have a single point domain, namely: u
,
w
, w_S00
, w_s01
, v_S00
and in the last two summands, y
.
These variables can be eliminated by applying sum elimination. For example: in
the first summand w
is equal to x
. Therefore w
can be substituted by
x
, and w
can then be removed from the sum since it is no longer used.
Applying sum elimination will give the following result:
proc P(x_P0: Bool) =
true -> delta
+ sum y_P0: Nat.(y_P0 < 6 && x_P0) ->b(y_P0 == 5) .P(!x_P0);
+ sum y_P0: Nat.(y_P0 < 6 && !(y_P0 == y_P0 * 2)) ->tau.P(!(y_P0 == y_P0 * 2))
+ (!x_P0 && x_P0) ->delta
+ sum y_P0: Nat.(((y_P0 < 6 && !x_P0) && !((y_P0 == y_P0 * 2) == x_P0)) &&
!(5 == y_P0)) -> a(x_P0, y_P0) .P(!x_P0)
Many action labels can be quickly renamed at once with a regular expression.
This regular expression has to be provided in the shape matching pattern/replacement
.
Note that this does not allow modification of action parameters.
The replacement pattern follows the standard of ECMAScript. Groups matched with
parentheses can be substituted in the replacement string using $n
, where
n
is the index of the matched group. See the
ECMAScript website
for more details.
We consider the following process:
proc P(s1: Pos) =
(s1 == 3) ->
a_out|c_out .
P(s1 = 2)
+ (s1 == 2) ->
b_out .
P(s1 = 1)
+ (s1 == 1) ->
c_out .
P(s1 = 4)
+ (s1 == 4) ->
delta;
We can remove the prefix of a_out
and c_out
using the regular expression
^([^b])_out$/$1
. To ensure the whole action name is matched, one may write
regular expressions in the shape ^expression$
.
It is also possible to rename actions to delta or to tau. For example, when
renaming a_out
to delta
using ^a_out$/delta
, the multi action
a_out|c_out
will become delta
. When applying the regex a_out/tau
,
the same multi-action becomes c_out
.
lpsactionrename [OPTION]... (--renamefile=NAME | --regex=EXPR) [INFILE [OUTFILE]]
Apply the action rename specification in FILE to the LPS in INFILE and save it to OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is not present, stdin is used.
-o
, --no-rewrite
do not rewrite data expressions while renaming; use when the rewrite system does not terminate
-m
, --no-sumelm
do not apply sum elimination to the final result
-t
, --no-typecheck
do not typecheck the resulting specfication
-QNUM
, --qlimit=NUM
limit enumeration of quantifiers to NUM iterations. (Default NUM=1000, NUM=0 for unlimited).
-eEXPR
, --regex=EXPR
use the provided regular expression to rename action labels. Argument should be of the shape ‘matching pattern/replacement’. Matched groups can be substituted in the result with $n, where n is the index of the group. It is generally good to surround the matching expression with ^$. Example: ‘^(.*)_send$/$1_receive’
-fNAME
, --renamefile=NAME
use the rename rules from NAME
-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
-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
--help-all
display help information, including hidden and experimental options
Jan Friso Groote and Tom Haenen