pbesabstract
Under- or overapproximate the solution of a PBES, by abstracting from variables.
Example
Consider the following PBES:
nu X(n:Nat) = val(n > 1000000) || X(n+1)
Computing X(0) depends on the computation of equations for all X(i),
for i <= 1000000. After pbesabstract, for variable n, the equation is
reduced to:
nu X(n:Nat) = false || X(n+1)
Now, an application of pbesparelm can detect the redundancy of variable
n, allowing one to rewrite the above equation to the equivalent PBES:
nu X = false || X
The latter is readily seen to have solution true. As a result, also the
original equation systems have result true.
Usage
pbesabstract [OPTION]... [INFILE [OUTFILE]]
Description
Reads a file containing a PBES. For the variables that are indicated to be abstracted, the smallest boolean subexpression is found which is then replaced by false (default) or true.
If the solution of a PBES after application of pbesabstract with the value false is true, then the original PBES has solution true. Similarly if the solution of a PBES after application of pbesabstract with the value true is false, then the original PBES has solution false. After abstracting from certain variables, pbesparelm can be used to remove these variables from the PBES hopefully, but not necessarily, reducing the number of BES variables required to solve the PBES.
If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.
Command line options
-a[NUM] , --abstraction-value[=NUM]
the abstraction value 0 (false) or 1 (true)
-iFORMAT , --in=FORMAT
use input format FORMAT:
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES in textual (mCRL2) format
-oFORMAT , --out=FORMAT
use output format FORMAT:
besBES in internal format
pbesPBES in internal format
pgsolverBES in PGSolver format
textPBES in textual (mCRL2) format
-f[PARAMS] , --select[=PARAMS]
select the PBES parameters that are allowed to be abstracted. Wild cards are allowed
Examples:
X1(b:Bool,c:Bool);X2(b:Bool) X1(:Bool);X2(:Bool) (:Bool)
--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