User manual/lpsuntime

From MCRL2

Remove time from an LPS.

Synopsis

lpsuntime [OPTION]... [INFILE [OUTFILE]]

Short description

The lpsuntime tool removes time from the linear process specification (LPS) in INFILE and writes the result to OUTFILE. IF INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

The process equation section of an LPS is of the following form:

proc P(d: D) = sum e_0: E_0. c_0(d,e_0) -> a_0(f_0(d,e_0)) @ t_0(d,e_0) . P(g_0(d,e_0))
             + sum e_1: E_1. c_1(d,e_1) -> a_1(f_1(d,e_1)) @ t_1(d,e_1) . P(g_1(d,e_1))
             + ...
             ;

The tool transforms this to the following equivalent untimed version:

proc P(d: D, t: Real) = sum e_0: E_0. (c_0(d,e_0) && t_0(d,e_0)) -> a_0(f_0(d,e_0)) . P(g_0(d,e_0),t_0(d,e_0))
                      + sum e_1: E_1. (c_1(d,e_1) && t_1(d,e_1)) -> a_1(f_1(d,e_1)) . P(g_1(d,e_1),t_1(d,e_1))
                      + ...
                      ;

Options

OPTION can be any of the following standard options:

-q, --quiet

do not display warning messages

-v, --verbose

display short intermediate messages

-d, --debug

display detailed intermediate messages

-h, --help

display help information

--version

display version information

Author

Written by Jeroen Keiren.

Bug reporting

Report bugs at our issue tracking system.

lpssuminst

lpsxsim