pbesabsinthe

Apply abstraction to the data domain of a PBES, based on user defined mappings.

Besides a PBES, the user must supply an input file, containing the following:

  • A partial data specification, that contains sorts and equations for the added abstractions.

  • An abstraction mapping of sorts, and an abstraction mapping of functions. The keywords absmap and absfunc are used for this. The symbol := is used to separate the left hand and the right hand sides of the mappings.

    sort
  AbsBit  = struct arbitrary;

var
  b:Bit;

eqn
  h(b) = arbitrary;
  abseq(arbitrary,arbitrary) = {true,false};
  absinv(arbitrary) = {arbitrary};

absmap
  h: Bit -> AbsBit;

absfunc
  ==: Bit # Bit -> Bool        := abseq : AbsBit # AbsBit -> Set(Bool);
  inv: Bit -> Bit              := absinv : AbsBit -> Set(AbsBit);

This file is passed to the tool using the option -a. The tool attempts to automatically generate abstractions of functions that were not specified by the user. The data specification and the right hand sides of the function mapping are merged with the data specification of the input PBES.

orphan:

Usage

pbesabsinthe   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and applies abstraction to it’s data domain, based on a user defined mappings. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

-aFILE , --abstraction-file=FILE

use the abstraction specification in FILE.

-l , --enable-logging

print absinthe specific log messages

-iFORMAT , --in=FORMAT

use input format FORMAT:

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-oFORMAT , --out=FORMAT

use output format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-sNAME , --strategy=NAME

use the approximation strategy NAME:

over

an over-approximation

under

an under-approximation

--timings[=FILE]

append timing measurements to FILE. Measurements are written to standard error if no FILE is provided

-u , --used-function-symbols

print used function symbols

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

Wieger Wesselink; Maciek Gazda and Tim Willemse