Skip to content

Commit

Permalink
Add documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@RipplB
RipplB committed Dec 17, 2024
1 parent d381042 commit 797b081
Show file tree
Hide file tree
Showing 9 changed files with 430 additions and 39 deletions.
20 changes: 20 additions & 0 deletions ...common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
## Overview

This package contains two new data structures, a Proof and a Cex.

### Abstract State Graph

`ASG` is a more simple state space representation than `ARG`. It works and is implemented in a very similar way,
except it does allow circles to appear in the graph.

### ASG trace

`ASGTrace` represents a lasso like trace, i.e. it is made with two parts: a tail and a loop. The loop is required
to start and end in the last state of the tail. This node in the graph is called honda.

### Visualization

The `ASGVisualizer` class (found in the `hu.bme.mit.theta.analysis.utils` package) provides visualization capabilities. Since it implements
the standard `ProofVisualizer` interface working on `ASG`s, the usage is fairly similar. Given an `ASG`, it returns a `hu.bme.mit.theta.common.visualization.Graph`
object that can be turned into actual visual representations (such as a Graphviz string with `hu.bme.mit.theta.common.visualization.writer.GraphvizWriter`
, which in turn can be displayed with external tools)
89 changes: 89 additions & 0 deletions ...nalysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
## Overview

This package provides algorithms that allow to look for accepting lasso shaped traces in a state space.
A lasso is a special form of trace, consisting of two parts: a tail and a loop. Both are like classic traces, where the
tail has to start from an initial state, and the loop has to start and end in the last state of the tail.
Loopchecker has to be provided with a predicate that can mark either states or actions as accepting. The loop checking
algorithms look for lasso traces that have such acceptance in their loop.

## Data structures

The data structures in Theta had a limitation that made them not suitable for the initial implementation of loopchecker.
Both ARG and Trace do not allow circles to appear in the state space. For this reason, loopchecker uses the
`hu.bme.mit.theta.analysis.algorithm.asg` package. The abstract state graph found in that package is suitable
for loop creation and detection, while the ASGTrace allows us to represent lasso shaped traces.

## Algorithms
For abstraction and trace concretization there are 2-2 algorithms, completely interchangeable. This is implemented
using the strategy design pattern.

### Abstraction

During abstraction, the `ASG` is built and explored until a valid `ASGTrace` is found. There are currently two algorithms
implemented, both based on a dept first search.

#### Nested Depth-First Search

NDFS contains of two Depth-First searches right after eachother to find a lasso trace. The goal of the first DFS
is to find any acceptance, and than the second should find the very same acceptance from there.

![]()


#### Guided depth first search

The basis of the
algorithm is Depth-First Search (DFS), where we do only one search with a modified
condition instead of two nested ones compared to NDFS. Let us call encountering an accepting state/transition an acceptance. In the DFS, while keeping an acceptance counter,
look for a node that is already on the stack and has a smaller value on the counter
than the top of the stack.

![]()


### Concretization

Concretizing a lasso trace requires an extra step after simple concretization. First the lasso is straightened to a classic
trace, and a classic concretization is used to determine if it's even feasible. However, after that, one needs to make
sure that the loop of the lasso is also a possible loop in the concrete state space.

#### Milano

This is a more direct approach. It checks whether the honda can be in the same
state before and after the loop. This is done by adding the cycle validity constraint to the
loop. An expression is added to the solver that requires all variables to have the same value in the first and
last state of the loop.

![]()

#### Bounded unrolling

The idea of bounded unwinding comes from E. Clarke et al., who defined an algorithm
to detect and refine lasso-shaped traces in the abstract state-space. The idea was that
even though we do not know if an abstract loop directly corresponds to a concrete loop,
we can be sure that the abstract loop can be concretized at most m different ways, where
m is the size of the smallest abstract state in the loop (if we think about abstract states as
sets of concrete states). That is because, if the loop is run m times and is concretizable,
the state that had the smallest number of concrete states has to repeat itself at least once.
The only limitations of the original algorithm were that it was defined for deterministic
operations only.

To slightly mitigate this limitation and be able to use the algorithm, we need to eliminate as many nondeterministic operations as possible. To achieve this, nondeterministic
operations have to be unfolded: they are replaced with all their possible deterministic
counterparts. For the nondet operations of `xsts`, this can be seen in the `XstsNormalizerPass` pass object.

Another limitation of the original algorithm in our context is that Theta is working with
possibly infinite domains, for which m could also potentially evaluate to infinite. To have a
chance to avoid these infinite unwindings, it is worth noting that counting all the concrete
states allowed by the abstract states in the loop is an overapproximation of the number
of all possible different states the concrete loop can reach. If a variable is included in only
such assignments (or no assignments at all) where the expression contains only literals,
that variable has a fixed value throughout the loop. That means, for such variables, just
one unwinding is enough.

To find all the variables that contribute towards the needed number of unwindings, `VarCollectorStatementVisitor` is used.
![]()

Since infinite bounds can
still be encountered, there is a configurable maximum for the bound. If m would be greater
than that, the refiner falls back to the default concretizer algorithm, which is Milano in the current implementation.
4 changes: 4 additions & 0 deletions subprojects/common/ltl-cli/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
## Overview
This package contains classes and objects related to CLIs that allow LTL model checking. For now it only contains a helper class
that is an implementation of the Clikt's package OptionGroup. This option group allows the user to select from the available
loopchecker and loop refinement strategies.
168 changes: 168 additions & 0 deletions subprojects/common/ltl/doc/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,168 @@
## Overview
This project has two main purposes. The `hu.bme.mit.theta.common.cfa.buchi` package is used to convert properties specified
in the LTL language to Buchi automata as CFA. The `hu.bme.mit.theta.common.ltl` package contains a SafetyChecker that
is able to perform LTL based model checking on any formalism.

## Supported LTL formulae

Currently the following LTL operators are supported in Theta:

| LTL operator | Symbol |
|----------------|--------|
| Eventually | F |
| Globally | G |
| Next | X |
| Until | U |
| Weak until | W |
| Release | R |
| Strong release | M |

On top of regular LTL, one can also use complex expressions over the simple variable types. See [Preprocessing](#preprocessing). For complex
examples, look at the [LtlCheckTestWithXstsPred test file](../src/test/kotlin/hu/bme/mit/theta/common/ltl/LtlCheckTestWithXstsPred.kt).


## Converting LTL to Buchi automaton

The main job is done by implementations of the `Ltl2BuchiTransformer` interface. This accepts an LTL formula and
produces a Buchi automaton in Theta representation. The current implementation `Ltl2BuchiThroughHoaf` does the following:

1. Preprocess the input LTL expression by substituting complex expressions with atomic propositions
2. Call a `Ltl2Hoaf` converter that produces the Buchi automaton in the [Hanoi Omega-Automata Format](https://adl.github.io/hoaf/)
3. Use the `BuchiBuilder` object to read the HOAF string and generate a CFA

![](ltl_conversion_pipeline.jpg)

### Preprocessing

Linear Temporal Logic works with atomic propositions, i.e. variables and expressions can only be of type boolean.
In align to this, most tools won't accept complex formulae, like `F(x == 9)`, i.e. _x is eventually going to become 9_.
To support such expressions, a preprocessing step is implemented. The entry point is in the `ToStringVisitor` class.
This class creates a new, now valid LTL expression with only atomic propositions, and provides a mapping from these
propositions to the original expressions. In our previoues example, the result could be `F p0`, and the mapping would contain
`p0 -> x == 9`.

### The purpose of [Hanoi Omega-Automata Format](https://adl.github.io/hoaf/) in the implementation

Since there were no tools or libraries that could have been linked due to licensing issues, it was required
to support calling external tools. HOAF is a standard that has many advantages for us:

* It's widely accepted and adopted by most of the tools related to LTL manipulation
* It's a rather stable but still maintained standard
* There is a library which is now included with theta that provides interfaces to work with HOAF

This allows the end-user to use any tool for the conversion they'd like. They only need to provided a command that runs on their system
and when the `ExternalLtl2Hoaf` runs it by appending the processed LTL formula after it, returns a Buchi automaton in the HOA format.

The recommended tools are [Spot](https://spot.lre.epita.fr/) and [Owl](https://owl.model.in.tum.de/).

#### Supported subset of HOAF

The current implementation has the following limitations on accepted HOAF strings:

| Limitation | Technical meaning | Related parser functions |
|-----------------------------------------------------|------------------------------------------------------------------------------------------------|---------------------------|
| Exactly one initial state is required | The string should contain exactly one `Start` header | addStartStates, notifyEnd |
| Only transition based acceptance is supported | The `acc-sig` in a state representation is ignored. Implicit labels cause an exception thrown. | addState, addEdgeImplicit |
| Only single acceptance set automatons are supported | The value of `acc-sig` on an edge is ignored. If any exists, the edge will be accepting | addEdgeWithLabel |

It is important to notice that the limitations around acceptances can silently fail and cause bad behaviour. This should be future work to properly check,
or better yet, support them.

### Why CFA?

Implementing Buchi automaton from scratch would have resulted in a lot of duplicate code with the already existing CFA class.
For this reason, CFA is now extended with optional accepting states or edges. Such CFA can perfectly model a Buchi automaton.

Of course, it would be more desirable, to have a common automaton superclass for CFA and a new Buchi automaton, but this was
not in scope for the project that developed these packages.

### Automated testing of LTL checking

Running external tools during automated testing such as in the CI/CD processes is not that feasible in the case of Theta.
For various reasons, our tests run on many different platforms. Running the above recommended programs during these tests
would result in a maintenance nightmare:

* The tools would need to be installed on all runner images
* Since most of them are only distributed for linux, calling them would require to be different on different operating systems
* For example, on windows you might use `WSL`, but the command `wsl` would of course fail on a linux system

For this reason, testing is done with another implementation of `Ltl2Hoaf`. `Ltl2HoafFromDir` is a class that expects
a directory as a parameter. Than when called with an LTL formula, encodes the formula to URL and looks up the resulting
filename.hoa in the directory.

### Architecture

The above interfaces and objects form the following architecture:

![](ltl2buchi.jpg)

## LTL checking

In the ltl package there is a single class the `LtlChecker`. This is a subclass of the safety checker, so it can fit
into most CLI algorithms easily. It uses the conversion mechanisms to create a Buchi automaton. Then uses the
`hu.bme.mit.theta.analysis.multi` package to create a product of this buchi automaton and the model that needs to
be checket. Finally it simply constructs a loopchecker abstractor and refiner, than builds
a `CegarChecker` with them.

For the details of the model checking algorithms, look at the `hu.bme.mit.theta.analysis.algorithm.loopchecker` package
in the common analysis subproject.

## How to run an LTL check

Currently only `xsts` models are supported with CLI execution. Run `xsts-cli` with the `LTLCEGAR` command to utilize it. The usage is the following:

### Input options

Options related to model and property input

| Option | Description |
|--------------------------------------------------|----------------------------------------------------------------------------------------------------|
| --model=<path> | Path of the input model (XSTS or Pnml). Extension should be .pnml to be handled as petri-net input |
| --property=<file> | Path of the property file. Has priority over |
| --inlineProperty | |
| --inline-property=<text> | Input property as a string. Ignored if --property is defined |
| --initialmarking=<text> | Initial marking of the pnml model |

### Output options

Options related to output and statistics

| Option | Description |
|----------------------------------------------------------------|-----------------------------------------------------|
| --log-level=(RESULT\|MAINSTEP\|SUBSTEP\|INFO\|DETAIL\|VERBOSE) | Detailedness of logging |
| --benchmark=true\|false | Quiet mode, output will be just the result metrics |
| --cexfile=<path> | Write concrete counterexample to a file |
| --stacktrace | Print stack trace of exceptions |
| --visualize=<path> | Write proof or counterexample to file in dot format |


### LTL options

Options related to LTL property checking

| Option | Description |
|------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------|
| --ltl-expression=<text> | LTL expression to check |
| --ltl2buchi-command=<text> | A command that runs on your system. The expression gets appended at the end of it.For example, if you use SPOT, this should be: spot ltl2tgba -f |
| --search-strategy=(GDFS\|NDFS\|FULL) | Which strategy to use for search |
| --refiner-strategy=(MILANO\|BOUNDED_UNROLLING) | Which strategy to use for concretization |
| --envtran-separation=(COMBINED\|SEPARATE) | Whether Buchi evaluation should happen between env and trans transitions or not (SEPARATED and COMBINED, respectively) |


### Options

Standard options


| Option | Description |
|------------------------------------------------------------------------------------------------------------------------|----------------------------------------|
| --version | Show the version and exit |
| --solver=<text> | The solver to use for the check |
| --smt-home=<path> | |
| --domain=(EXPL\|PRED_BOOL\|PRED_CART\|PRED_SPLIT\|EXPL_PRED_BOOL\|EXPL_PRED_CART\|EXPL_PRED_SPLIT\|EXPL_PRED_COMBINED) | Abstraction domain to use |
| --refinement=(FW_BIN_ITP\|BW_BIN_ITP\|SEQ_ITP\|UNSAT_CORE\|MULTI_SEQ) | Refinement strategy to use |
| --predsplit=(WHOLE\|CONJUNCTS\|ATOMS) | |
| --refinement-solver=<text> | Use a different solver for abstraction |
| --abstraction-solver=<text> | Use a different solver for refinement |
| --initprec=(EMPTY\|PROP\|CTRL\|ALLVARS) | Initial precision |

Loading

0 comments on commit 797b081

Please sign in to comment.