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.

Manual page for pbesabsinthe

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-fileFILE

use the abstraction specification in FILE.

-l , --enable-logging

print absinthe specific log messages

-iFORMAT , --inFORMAT

use input format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-oFORMAT , --outFORMAT

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 , --strategyNAME

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 intermediate messages

-d , --debug

display detailed intermediate messages

--log-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Wieger Wesselink; Maciek Gazda and Tim Willemse