Commit a253c79b authored by Simon Prucker's avatar Simon Prucker
Browse files

replace formula parser

parent 3e958dab
Pipeline #16020 waiting for manual action with stages
in 16 seconds
......@@ -11,11 +11,11 @@ COOL is a generic reasoner for modal, hybrid and fixpoint logics, developed join
Visit the [release page](https://git8.cs.fau.de/software/cool/-/releases) to get released versions of COOL.
We provide multiple options to get your hands on an up to date COOL executables:
We provide multiple options to get your hands on an up to date COOL executable:
- Docker images on Dockerhub as `cs8service/cool` tagged with the branch they were published from i.e. `cs8service/cool:master` would give you the latest release candidate of COOL.
You could e.g. use it to check coalition logic formulas `echo '<{1 2}> C & [{1 2}] ~C' | docker run -i cs8service/cool:master sat CL`
- A prebuilt static binary of the latest release candidate is available as [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/master/browse/cool-static?job=nix-build).
Run it e.g. `coalg sat CL <<< '<{1 2}> C & [{1 2}] ~C'`
Run it e.g. `cool-coalg sat CL <<< '<{1 2}> C & [{1 2}] ~C'`
- Dynamically linked executables without included dependencies are also available [in the artefacts](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/master/browse/dynamic?job=build).
There are additional features yet to be merged so use at your own risk:
......@@ -23,7 +23,7 @@ There are additional features yet to be merged so use at your own risk:
#### Modelchecking
If you want to do modelchecking you should look into [the `modcheck` branch](https://git8.cs.fau.de/software/cool/-/tree/modcheck) and the related artefacts:
- Docker images unter `cs8service/cool:modcheck`
- Docker images at `cs8service/cool:modcheck`
- [`cool-static`](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/modcheck/browse/cool-static?job=nix-build)
- [Dynamically linked executables](https://git8.cs.fau.de/software/cool/-/jobs/artifacts/modcheck/browse/dynamic?job=build).
......@@ -31,7 +31,7 @@ If you want to do modelchecking you should look into [the `modcheck` branch](htt
We also provide batteries included build infrastructure using `nix`. See [the respective documentation](./nix/) on how to use `nix` to develop or compile COOL.
You could compile and intall COOL and all it's dependencies using `nix` by running `nix-env -f https://git8.cs.fau.de/software/cool/-/archive/master/cool-master.tar.gz -iA cool`
You could compile and install COOL and all it's dependencies using `nix` by running `nix-env -f https://git8.cs.fau.de/software/cool/-/archive/master/cool-master.tar.gz -iA cool`
### Dependencies
......@@ -54,7 +54,7 @@ dune build
```
Run it with
```
dune exec cool
dune exec cool-coalg
```
To build everything just run
```
......@@ -79,11 +79,11 @@ cd cool
dune build @all
```
## Usage
## More Examples
To see a longer list of example formulas, just run the testsuite:
To see a longer list of example formulas, just have a look at the files at
```
dune exec cool-testsuite
./lib/tests/testsuite
```
### Coalition Logic
......@@ -101,7 +101,7 @@ Some formulas are
So call for example:
```bash
./coalg sat CL <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
./cool-coalg sat CL <<< '<{ 1 2 }> C & [{ 1 2 }] ~C'
# or via docker
echo '<{1 2}> C & [{1 2}] ~C' | docker run -i cs8service/cool:master sat CL
```
......
......@@ -2613,4 +2613,6 @@ let rec parseFormulaToTree formula =
| EB (f1, f2) -> let (child1, child2) = (parseFormulaToTree f1, parseFormulaToTree f2) in
Node ([child1; child2], (fun fList -> EB (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
let formula_of_string expr =
FormulaParser.formula FormulaLexer.lex (Lexing.from_string expr)
(* vim: set et sw=2 sts=2 ts=8 : *)
......@@ -193,4 +193,6 @@ Parses a formula into a tree representation, where each node contains a connecti
**)
val parseFormulaToTree: formula -> formula CoolUtils.Tree.tree
val formula_of_string: string -> formula
(* vim: set et sw=2 sts=2 ts=8 : *)
......@@ -9,7 +9,7 @@ open OUnit2
let isMuAconjunctive_test _ =
let with_formula str action = action (importFormula str) str in
let with_formula str action = action (formula_of_string str) str in
with_formula "ν x. ν y. ([r] x & <r> y)" (fun f f_str ->
assert_bool f_str (isMuAconjunctive f));
......@@ -27,9 +27,6 @@ let treeParserAndSimplify_prop =
let printAndParseInverse_predicate formula =
string_of_formula (FormulaParser.formula FormulaLexer.lex (Lexing.from_string (string_of_formula formula))) = string_of_formula formula
(*let printAndParseInverse_predicate formula =
importFormula (string_of_formula (importFormula (string_of_formula formula))) = importFormula (string_of_formula formula)*)
let printAndParseInverse_prop =
"printAndParseInverse" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:300
(make ~print:string_of_formula (sized Formula_gen.formula_Any)) printAndParseInverse_predicate)
......
......@@ -10,6 +10,6 @@ dockerTools.buildImage {
contents = cool;
config = {
Entrypoint = [ "/bin/coalg" ];
Entrypoint = [ "/bin/cool-coalg" ];
};
}
......@@ -251,7 +251,7 @@ let choicePrint _opts =
while true do
let input = read_line () in
if not (GenAndComp.isEmptyString input) then
let f = CoAlgFormula.importFormula input in
let f = CoAlgFormula.formula_of_string input in
let str = CoAlgFormula.exportFormula f in
incr counter;
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
......@@ -320,7 +320,7 @@ let choiceNNF _opts =
while true do
let input = read_line () in
if not (GenAndComp.isEmptyString input) then
let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in
let f = CoAlgFormula.nnf (CoAlgFormula.formula_of_string input) in
let str = CoAlgFormula.exportFormula f in
incr counter;
print_string (str ^ "\n");
......@@ -343,7 +343,7 @@ let choiceVerify _opts =
print_string "> ";
let input = read_line () in
if not (GenAndComp.isEmptyString input) then
let f = CoAlgFormula.importFormula input in
let f = CoAlgFormula.formula_of_string input in
let str = CoAlgFormula.exportFormula f in
incr counter;
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment