Attestor Benchmark Collection
This is a collection of examples accompanying Attestor based on the JMH benchmark framework.
Before running examples, please make sure that the benchmark project is installed by running the following command from within this directory:
mvn clean install
To execute all benchmarks once, it then suffices to run
For a more accurate performance measurement, please use the following command instead:
Since the last command runs every example multiple times, please note that a full performance measurement might require a lot of time.
Structure of Benchmarks
All benchmarks are defined in
Every Java class in this directory represents one group of benchmarks. Every method in one of these classes specifies a single benchmark (using the JMH framework). The name of the method must coincide with a corresponding settings file found in
CLASSNAME is the name of the Java class defining a group of examples.
Every settings file specifies the actual benchmark. This includes:
- The analyzed source code, which is usually found in
- The LTL specification verified by the tool.
- The graph grammars used to guide abstraction. User-specified graph-grammars are found in
CLASSNAME/configuration/grammar. For predefined grammars, such as binary trees, this directory may also contain renaming classes to map node and edge labels to class names and member variables.
- The initial heap in case the input is not supposed to be empty, e.g. when analyzing a procedure with parameters.
These heaps are found in
- A description of the benchmark and verified properties (see
- Command-line options, such as the maximal number of states until the tool aborts state space generation.
- The relevant paths to export a generated state space for the graphical user interface.
For example, the benchmark method
lindstromTraverse executes the benchmark described in the file
Every benchmark may additionally specify expected outcomes, e.g. whether provided specifications are expected to be satisfied or not.