Skip to content
Snippets Groups Projects
Commit 6c8a2f0c authored by Jaime Arias's avatar Jaime Arias
Browse files

add progressive option only for on-the-fly mc

parent 83297177
Branches main
No related tags found
1 merge request!4Improve the CLI
Pipeline #4846 passed with stage
in 1 minute and 26 seconds
......@@ -56,8 +56,6 @@ Options:
--ltl Path:FILE REQUIRED LTL property file
--thread TEXT:{posix,c++} Thread library (default: c++)
--por,--no-por{false} Apply partial order reductions (default: false)
--progressive,--no-progressive{false} Excludes: --explicit
Use a progressive construction of the SOG (default: false)
Explicit MC:
......@@ -72,6 +70,8 @@ Explicit MC:
On-the-fly MC:
--progressive,--no-progressive{false} Excludes: --explicit
Use a progressive construction of the SOG (default: false)
--emptiness-check TEXT Excludes: --explicit
Spot emptiness-check algorithm
......@@ -81,9 +81,9 @@ Print:
--dot-formula Save the automata of the negated formula in a dot file
--counter-example Needs: --explicit
Save the counter example in a dot file
```
### Emptiness-Check algorithms
The emptiness-check algorithms are provided by spot. For more information,
please see https://spot.lrde.epita.fr/doxygen/group__emptiness__check.html.
Here, some of examples:
......
......@@ -416,7 +416,7 @@ int main(int argc, char **argv)
// progressive construction can be used only when using on-the-fly model-checking
bool progressive{false};
app.add_flag("--progressive,!--no-progressive", progressive, "Use a progressive construction of the SOG (default: false)")->excludes(exp_opt);
app.add_flag("--progressive,!--no-progressive", progressive, "Use a progressive construction of the SOG (default: false)")->excludes(exp_opt)->group("On-the-fly MC");
// emptiness check algorithm is only needed when using on-the-fly model-checking
string algorithm = "";
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment