diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md new file mode 100644 index 0000000000..5716f7d109 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/asg/README.md @@ -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) \ No newline at end of file diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md new file mode 100644 index 0000000000..55a0d22053 --- /dev/null +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/loopchecker/README.md @@ -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. diff --git a/subprojects/common/ltl-cli/README.md b/subprojects/common/ltl-cli/README.md new file mode 100644 index 0000000000..f839575586 --- /dev/null +++ b/subprojects/common/ltl-cli/README.md @@ -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. \ No newline at end of file diff --git a/subprojects/common/ltl/doc/README.md b/subprojects/common/ltl/doc/README.md new file mode 100644 index 0000000000..c3da9a07a6 --- /dev/null +++ b/subprojects/common/ltl/doc/README.md @@ -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 of the input model (XSTS or Pnml). Extension should be .pnml to be handled as petri-net input | +| --property= | Path of the property file. Has priority over | +| --inlineProperty | | +| --inline-property= | Input property as a string. Ignored if --property is defined | +| --initialmarking= | 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= | Write concrete counterexample to a file | +| --stacktrace | Print stack trace of exceptions | +| --visualize= | Write proof or counterexample to file in dot format | + + +### LTL options + +Options related to LTL property checking + +| Option | Description | +|------------------------------------------------|--------------------------------------------------------------------------------------------------------------------------------------------------| +| --ltl-expression= | LTL expression to check | +| --ltl2buchi-command= | 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= | The solver to use for the check | +| --smt-home= | | +| --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= | Use a different solver for abstraction | +| --abstraction-solver= | Use a different solver for refinement | +| --initprec=(EMPTY\|PROP\|CTRL\|ALLVARS) | Initial precision | + diff --git a/subprojects/common/ltl/doc/ltl2buchi.drawio b/subprojects/common/ltl/doc/ltl2buchi.drawio new file mode 100644 index 0000000000..27f8690cb9 --- /dev/null +++ b/subprojects/common/ltl/doc/ltl2buchi.drawio @@ -0,0 +1,70 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/subprojects/common/ltl/doc/ltl2buchi.jpg b/subprojects/common/ltl/doc/ltl2buchi.jpg new file mode 100644 index 0000000000..f58d526a38 Binary files /dev/null and b/subprojects/common/ltl/doc/ltl2buchi.jpg differ diff --git a/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio b/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio new file mode 100644 index 0000000000..a908f9a612 --- /dev/null +++ b/subprojects/common/ltl/doc/ltl_conversion_pipeline.drawio @@ -0,0 +1,31 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg b/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg new file mode 100644 index 0000000000..b36fa27f40 Binary files /dev/null and b/subprojects/common/ltl/doc/ltl_conversion_pipeline.jpg differ diff --git a/subprojects/xsts/xsts-cli/README.md b/subprojects/xsts/xsts-cli/README.md index 0054a2175d..32ec44206f 100644 --- a/subprojects/xsts/xsts-cli/README.md +++ b/subprojects/xsts/xsts-cli/README.md @@ -28,12 +28,13 @@ the [`xsts`](../xsts/README.md) project. 2. Running the tool requires Java (JRE) 17. 3. The tool also requires the [Z3 SMT solver libraries](../../../doc/Build.md) to be available on `PATH`. -4. The tool can be executed with `java -jar theta-xsts-cli.jar [ARGUMENTS]`. +4. The tool can be executed with `java -jar theta-xsts-cli.jar [SUBCOMMAND] [ARGUMENTS]`. + * SUBCOMMAND should be the algorithm you want to run (Previous commands with the `--algorithm` switch should move the value here) * If no arguments are given, a help screen is displayed about the arguments and their possible values. More information can also be found below. * For - example `java -jar theta-xsts-cli.jar --model crossroad.xsts --property "x>1" --loglevel INFO` + example `java -jar theta-xsts-cli.jar CEGAR --model crossroad.xsts --property "x>1" --loglevel INFO` runs the default analysis with logging on the `crossroad.xsts` model file with the property `x>1`. @@ -55,40 +56,48 @@ residing on the host: Note that the model must be given as the first positional argument (without `--model`). -## Arguments - -All arguments are optional, except `--model` and `--property`. - -* `--model`: Path of the input XSTS model (mandatory). Can also accept PNML files with the `*.pnml` - extension. -* `--property`: Input property as a string or a file (*.prop) (mandatory). For PNML models an unsafe - target marking can also be described by listing the values of each place in their order of - definition separated with spaces. -* `--cex`: Output file where the counterexample is written (if the result is unsafe). If the - argument is not given (default) the counterexample is not printed. Use `CON` (Windows) - or `/dev/stdout` (Linux) as argument to print to the standard output. -* `--loglevel`: Detailedness of logging. - * Possible values (from the least to the most detailed): `RESULT`, `MAINSTEP`, `SUBSTEP` ( - default), `INFO`, `DETAIL`, `VERBOSE`. -* `--version`: Print version info (in this case `--model` and `--property` is of course not - required). -* `--metrics`: Print metrics about the XSTS model (number of variables and statements). -* `--initialmarking`: Can be used with the PNML frontend. Override the initial markings of the - places. Format: list the values to be assigned to each place in the order of their definition in - the PNML file separated with spaces. -* `--visualize`: Visualize the result of the analysis (the reachability graph if the model is safe, - or a counterexample trace if it is unsafe). Prints to the dotfile given as parameter. -* `--optimizestmts`: The algorithm can optimize stmts by detecting failing assumptions and - unreachable branches of choices. - * Possible values: `ON` (default), `OFF`. - -The arguments related to the algorithm are described in more detail (along with best practices) -in [CEGAR-algorithms.md](../../../doc/CEGAR-algorithms.md). - -### For developer usage - -| Flag | Description | -|----------------|-----------------------------------------------------| -| `--stacktrace` | Print full stack trace for exceptions. | -| `--benchmark` | Benchmark mode, only print metrics in csv format. | -| `--header` | Print the header for the benchmark mode csv format. | +## Subcommands +There are two categories of subcommands, one for model checking and one for helper texts. For up to date information, run the +CLI without any subcommand, or with the `--help` flag and the available subcommands will be printed for you. +### Algorithms +The following subcommands are available as arguments: + +| **Feature** | **Description** | +|---------------------|----------------------------------------------------------------------------------------------------------------------------------| +| **CEGAR** | Model checking using the CEGAR (CounterExample Guided Abstraction Refinement) algorithm | +| **LTLCEGAR** | Model checking using the CEGAR algorithm with an LTL property | +| **BOUNDED** | Bounded model checking algorithms (BMC, IMC, KINDUCTION). Use `--variant` to select the algorithm (by default, BMC is selected). | +| **MDD** | Model checking of XSTS using MDDs (Multi-value Decision Diagrams) | +| **PN_MDD** | Model checking of Petri nets using MDDs (Multi-value Decision Diagrams) | +| **CHC** | Model checking using the Horn solving backend | + +### Helper commands +There are two subcommands that simply output information: + +* **header** : Used to print a header for outputs generated by the `--benchmark` option in the algorithm commands. If you are doing +a larger benchmark with multiple runs piping into a file, this can be run first to provide a header for the file +* **metrics** : Prints information about the input xsts model + +## Common arguments + +There is two group of arguments that are mostly common among all the algorithm subcommands. + +### Input options +Options related to model and property input + +| **Option** | **Description** | +|----------------------------|-------------------------------------------------------------------------------------------------------------| +| `--model=` | Path of the input model (XSTS or Pnml). Extension should be `.pnml` to be handled as Petri-net input | +| `--property=` | Path of the property file. Has priority over `--inlineProperty` | +| `--inline-property=` | Input property as a string. Ignored if `--property` is defined | + +### Output options +Options related to output and statistics + +| **Option** | **Description** | +|------------------------|--------------------------------------------------------------------------------------------------------| +| `--log-level=` | Detailedness of logging. Possible values: `RESULT`, `MAINSTEP`, `SUBSTEP`, `INFO`, `DETAIL`, `VERBOSE` | +| `--benchmark=` | Quiet mode, output will be just the result metrics. Possible values: `true`, `false` | +| `--cexfile=` | Write concrete counterexample to a file | +| `--stacktrace` | Print stack trace of exceptions | +| `--visualize=` | Write proof or counterexample to file in DOT format |