Skip to content
GitLab
Commit eaf6ecb3 authored by Merlin's avatar Merlin 💧
Browse files

Merge branch 'refactoring' into 'master' 

Refactoring

Closes #37 and #21

See merge request !10
parents 88a4a2e4 85024dee
Pipeline #16043 passed with stages
in 96 minutes and 47 seconds
Hide whitespace changes
Inline Side-by-side
.gitlab-ci.yml
View file @ eaf6ecb3
......@@ -118,6 +118,6 @@ cross:
- cd src/exes && dune build --profile=static
parallel:
matrix:
- OCAML_VERSION: ["4.07", "4.08", "4.09", "4.10", "4.11", "4.12", "4.13", "4.14"]
- OCAML_VERSION: ["4.07", "4.08", "4.09", "4.10", "4.11", "4.12", "4.13", "4.14", "5.0", "5.1"]
README.md
View file @ eaf6ecb3
......@@ -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
```
......
ci/ocaml-setup.sh
View file @ eaf6ecb3
......@@ -4,4 +4,4 @@ if ! type "opam" > /dev/null; then
sudo apt-get install -y opam
fi
opam update
opam install -y dune ocamlfind ocamlgraph ounit pgsolver ocamline "qcheck>=0.15"
opam install -y dune ocamlfind ocamlgraph ounit pgsolver ocamline "qcheck>=0.15" camlp-streams menhir
default.nix
View file @ eaf6ecb3
......@@ -39,6 +39,6 @@ with nixpkgs; rec {
cool-devenv = mkShell {
inputsFrom = [ cool cool-lib cool-generators ];
packages = with ocamlPackages; [ ocaml-lsp dune_2 ];
packages = with ocamlPackages; [ ocaml-lsp dune_3 menhir ];
};
}
dune-workspace
View file @ eaf6ecb3
......@@ -4,6 +4,8 @@
;; 8: unused value as somethimes code is left over or for future use
;; 24: bad module name as our executables are not modules and we dont care
;; 32: unmatched values warnings are sometimes intentional
;; 67: unused functor parameter (as it seems to occur by error in some compiler versions)
;; 69: unused record field (as it seems to occur by error in some compiler versions)
(env
(dev
(flags (:standard -w -6-8-24-32-67 -alert -all--all))))
(flags (:standard -w -6-8-24-32-67-69))))
lib/dune-project
View file @ eaf6ecb3
(lang dune 1.11)
(using menhir 2.0)
(name cool-lib)
(version 2.1)
lib/src/CoAlgFormula.ml
View file @ eaf6ecb3
......@@ -2614,3 +2614,5 @@ let rec parseFormulaToTree formula =
Node ([child1; child2], (fun fList -> EB (List.hd fList, List.nth fList 1)), (max (getHeight child1) (getHeight child2)) + 1)
(* vim: set et sw=2 sts=2 ts=8 : *)
\ No newline at end of file
lib/src/FunctorParsing.ml → lib/src/CoolParser.ml
View file @ eaf6ecb3
(**Parsing formulae to strings*)
let formula_of_string expr =
FormulaParser.formula FormulaLexer.lex (Lexing.from_string expr)
(**Part from former FunctorParsing module*)
(* Parsing strings to sort tables *)
open Stdlib
module CM = CoAlgMisc
type functorExp =
......
lib/src/FunctorParsing.mli → lib/src/CoolParser.mli
View file @ eaf6ecb3
val formula_of_string: string -> CoAlgFormula.formula
(**Part from former FunctorParsing module*)
(* Parsing strings to sort tables *)
type functorExp =
......
lib/src/CoolUtils.mli
View file @ eaf6ecb3
......@@ -109,4 +109,5 @@ module Tree :
val getHeight : 'a tree -> int
end
(* vim: set et sw=2 sts=2 ts=8 : *)
lib/src/FormulaLexer.mll 0 → 100644
View file @ eaf6ecb3
{
exception Error of string
}
let al = ['a'-'z' 'A'-'Z']
let num = ['0'-'9']
let alnum = (al|num)+
let id = ['a' - 'z'] (alnum)?
let nat0 = num+
rule lex = parse
[' ' '\t' '\n']+ {lex lexbuf}
| ("True"|"TRUE"|"true"|"T"|"Top"|"TOP"|"top"|"Verum"|"verum"|"VERUM"|"⊤") {FormulaParser.True}
| ("False"| "FALSE"|"false"|"F"|"Bottom"|"bottom"|"BOTTOM"|"Falsum"|"falsum"|"FALSUM"|"⊥") {FormulaParser.False}
| ("~"|"¬") {FormulaParser.Not}
| ("=>"|"->"|"→"|"⇒"|"-->"|"==>") {FormulaParser.Implies}
| ('&'|"/\\"|"&&"|"∧"|"·") {FormulaParser.And}
| ('|'|"+"|"∨") {FormulaParser.Or}
| ("<=>"|"<->"|"⇔"|"↔") {FormulaParser.Equiv}
| '<' {FormulaParser.DiaOpen}
| '>' {FormulaParser.DiaClose}
| '[' {FormulaParser.BoxOpen}
| ']' {FormulaParser.BoxClose}
| '(' {FormulaParser.LBrace}
| ')' {FormulaParser.RBrace}
| '{' {FormulaParser.CLBrace}
| '}' {FormulaParser.CRBrace}
| "AG" {FormulaParser.AG}
| "AF" {FormulaParser.AF}
| "EF" {FormulaParser.EF}
| "EG" {FormulaParser.EG}
| 'E' {FormulaParser.E}
| 'A' {FormulaParser.A}
| 'B' {FormulaParser.B}
| 'U' {FormulaParser.U}
| 'R' {FormulaParser.R}
| ("MY"|"MU"|"Mu"|"My"|"µ"|"μ") {FormulaParser.MY}
| ("NY"|"NU"|"Nu"|"Ny"|"ν"|"ν") {FormulaParser.NY}
| '.' {FormulaParser.Dot}
| id as s {FormulaParser.Identifyer s}
| nat0 as n {FormulaParser.Nat0 (int_of_string n)}
| eof {FormulaParser.EOF}
lib/src/FormulaParser.mly 0 → 100644
View file @ eaf6ecb3
%{
let fpVars = ref []
%}
%token And
%token Or
%token Not
%token Implies
%token Equiv
%token DiaOpen
%token BoxOpen
%token DiaClose
%token BoxClose
%token True
%token False
%token CLBrace /*Curly Left Brace*/
%token CRBrace
%token RBrace
%token LBrace
%token Dot
%token EF
%token AF
%token AG
%token EG
%token E
%token A
%token B
%token U
%token R
%token MY
%token NY
%token <string> Identifyer
%token <int> Nat0
%token EOF
%start <CoAlgFormula.formula> formula
/*%type <CoAlgFormula.formula> formula prec0 prec1 prec2 prec3 prec4
%type <int list> natSeq*/
%%
%inline braced(Inner):
a = delimited(LBrace, Inner, RBrace) {a}
%inline dia(Inner):
a = delimited(DiaOpen, Inner, DiaClose) {a}
%inline box(Inner):
a = delimited(BoxOpen, Inner, BoxClose) {a}
%inline curlied(Inner):
a = delimited(CLBrace, Inner, CRBrace) {a}
formula:
| a = prec0 EOF {a}
;
prec0_5:
| a = prec1 Implies b = prec0_5 {CoAlgFormula.IMP (a, b)}
| a = prec1 {a}
| a = braced(prec0) {a}
prec0:
| a = prec0_5 Equiv b = prec0 {CoAlgFormula.EQU (a, b)}
| a = prec0_5 {a}
| a = braced(prec0) {a}
;
prec1:
| a = prec2 Or b = prec1 {CoAlgFormula.OR (a,b)}
| a = prec2 {a}
| a = braced(prec0) {a}
;
prec2:
| a = prec3 And b = prec2 {CoAlgFormula.AND (a,b)}
| a = prec3 {a}
| a = braced(prec0) {a}
;
%inline ctlPathQuant:
| A {`a}
| E {`e}
%inline ctlPathDelim:
| U {`u}
| R {`r}
| B {`b}
%inline ctlSplitFormula:
| p = ctlPathQuant i = braced(a = prec0 d = ctlPathDelim b = prec0 {(d, (a, b))}) { match (p, i) with
| (`a, (`u, (x, y))) -> CoAlgFormula.AU (x, y)
| (`a, (`r, (x, y))) -> CoAlgFormula.AR (x, y)
| (`a, (`b, (x, y))) -> CoAlgFormula.AB (x, y)
| (`e, (`u, (x, y))) -> CoAlgFormula.EU (x, y)
| (`e, (`r, (x, y))) -> CoAlgFormula.ER (x, y)
| (`e, (`b, (x, y))) -> CoAlgFormula.EB (x, y)
}
prec3:
| MY a = Identifyer Dot b = prec3 {fpVars := a :: !fpVars ;CoAlgFormula.MU (a, b)}
| NY a = Identifyer Dot b = prec3 {fpVars := a :: !fpVars ;CoAlgFormula.NU (a, b)}
| a = ctlSplitFormula {a}
| AF a = prec3 {CoAlgFormula.AF a}
| AG a = prec3 {CoAlgFormula.AG a}
| EF a = prec3 {CoAlgFormula.EF a}
| EG a = prec3 {CoAlgFormula.EG a}
| Not a = prec3 {CoAlgFormula.NOT a}
| m = dia(Identifyer) a = prec3 {CoAlgFormula.EX (m, a)}
| DiaOpen DiaClose a = prec3 {CoAlgFormula.EX ("unimod", a)}
| mn = dia(m = Nat0 n = Identifyer {(m,n)}) a = prec3 {CoAlgFormula.MORETHAN (fst mn, snd mn, a)}
| m = dia(curlied(Nat0*)) a = prec3 {CoAlgFormula.ALLOWS (m, a)}
| m = box(Identifyer) a = prec3 {CoAlgFormula.AX (m, a)}
| BoxOpen BoxClose a = prec3 {CoAlgFormula.AX ("unimod", a)}
| mn = box(m = Nat0 n = Identifyer {(m,n)}) a = prec3 {CoAlgFormula.MAXEXCEPT (fst mn, snd mn, a)}
| m = box(curlied(Nat0*)) a = prec3 {CoAlgFormula.ENFORCES (m, a)}
| a = prec4 {a}
| a = braced(prec0) {a}
;
prec4:
| a = Identifyer {if (List.mem a !fpVars) then CoAlgFormula.VAR a else CoAlgFormula.AP a}
| True {CoAlgFormula.TRUE}
| False {CoAlgFormula.FALSE}
;
%%
lib/src/dune
View file @ eaf6ecb3
......@@ -6,4 +6,10 @@
(cxx_names "minisat_stub")
(cxx_flags "-std=c++98" "-fPIC")
(c_library_flags "-lminisat -lstdc++")
(libraries ocamlgraph unix str pgsolver))
(libraries ocamlgraph unix str pgsolver camlp-streams))
(menhir
(modules FormulaParser)
(flags --explain))
(ocamllex FormulaLexer)
\ No newline at end of file
lib/tests/testsuite/Testsuite.ml
View file @ eaf6ecb3
......@@ -5,7 +5,7 @@ open QCheck
(*open QCheck.Gen*)
open QCheck_ounit
module F = CoAlgFormula
module FP = FunctorParsing
module FP = CoolParser
module FG = Formula_gen
module G = CoolGraph
module CR = CoAlgReasoner
......
lib/tests/testsuite/cool_testsuite.ml
View file @ eaf6ecb3
......@@ -3,7 +3,7 @@ open OUnit2
open Testsuite
module DL98 = DL98TestCases
module CTL = CTLTestCases
module FE = FunctorParsing
module FE = CoolParser
module CM = CoAlgMisc
module FG = Formula_gen
......
lib/tests/unit_tests/CoAlgFormula_tests.ml
View file @ eaf6ecb3
......@@ -7,8 +7,9 @@ open OUnit2
let isMuAconjunctive_test _ =
let with_formula str action = action (importFormula str) str in
let with_formula str action = action (CoolParser.formula_of_string str) str in
with_formula "ν x. ν y. ([r] x & <r> y)" (fun f f_str ->
assert_bool f_str (isMuAconjunctive f));
......@@ -23,21 +24,17 @@ let treeParserAndSimplify_predicate formula =
let treeParserAndSimplify_prop =
"treeParserAndSimplify" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000 ( make (sized Formula_gen.formula_K)) treeParserAndSimplify_predicate)
let printAndParseInverse_predicate formula =
importFormula (string_of_formula (importFormula (string_of_formula formula))) = importFormula (string_of_formula formula)
let printAndParseInverse_predicate formula =
string_of_formula (FormulaParser.formula FormulaLexer.lex (Lexing.from_string (string_of_formula formula))) = string_of_formula formula
let printAndParseInverse_prop =
"printAndParseInverse" >: to_ounit2_test ~rand:(Random.State.make_self_init ()) (Test.make ~count:10000
(make (oneof [sized Formula_gen.formula_GML; sized Formula_gen.formula_CL]
(*
[(sized ((fun x -> (CoolUtils.curry (Formula_gen.formula_fp x) [])) Formula_gen.gmlFormula));
(sized ((fun x -> (CoolUtils.curry (Formula_gen.formula_fp x) [])) Formula_gen.clFormula));
(sized (Formula_gen.formula_ctl Formula_gen.gmlFormula));
(sized (Formula_gen.formula_ctl Formula_gen.clFormula))]
*)
)) printAndParseInverse_predicate)
let tests = "CoAlgFormula" >::: ["isMuAconjunctive" >:: isMuAconjunctive_test; "treeParserAndSimplify" >: treeParserAndSimplify_prop; "printAndParseInverse" >: 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)
let tests = "CoAlgFormula" >::: [ "isMuAconjunctive" >:: isMuAconjunctive_test
; "treeParserAndSimplify" >: treeParserAndSimplify_prop
; "printAndParseInverse" >: printAndParseInverse_prop
]
(* vim: set et sw=2 sts=2 ts=8 : *)
lib/tests/unit_tests/CoAlgMisc_tests.ml
View file @ eaf6ecb3
......@@ -17,7 +17,7 @@ let alternationLevel_test _ =
let formulaAlternationLevel_test _ =
let wrapper formula subformula =
sortTable := FunctorParsing.sortTableFromString "K";
sortTable := CoolParser.sortTableFromString "K";
let hcF = C.HcFormula.create true in
let hcf = C.hc_formula hcF formula in
let nomTbl _ = Some 0 in
......
nix/cool-docker.nix
View file @ eaf6ecb3
......@@ -10,6 +10,6 @@ dockerTools.buildImage {
contents = cool;
config = {
Entrypoint = [ "/bin/coalg" ];
Entrypoint = [ "/bin/cool-coalg" ];
};
}
nix/cool-lib.nix
View file @ eaf6ecb3
{ lib, buildDunePackage, qcheck, ounit, cool-generators, ocamlgraph, fetchgit, pgsolver, glibc, zlib, minisat, ocamline, profile ? null, versions, doCheck ? true }:
{ lib, buildDunePackage, qcheck, ounit, camlp-streams, cool-generators, ocamlgraph, fetchgit, pgsolver, glibc, zlib, minisat, ocamline, menhir, profile ? null, versions, doCheck ? true }:
buildDunePackage ({
pname = "cool-lib";
......@@ -9,8 +9,8 @@ buildDunePackage ({
src = ../lib;
buildInputs = [ zlib.dev minisat glibc];
propagatedBuildInputs = [ ocamlgraph pgsolver ocamline];
buildInputs = [ zlib.dev minisat glibc menhir ];
propagatedBuildInputs = [ ocamlgraph pgsolver ocamline camlp-streams ];
# buildPhase = ''
# runHook preBuild
......
nix/cool-metrics.nix
View file @ eaf6ecb3
......@@ -8,7 +8,7 @@ stdenv.mkDerivation {
buildInputs = [ hyperfine cool (python3.withPackages (p : [ p.numpy ])) ];
buildPhase = ''
hyperfine 'cat metric_formulas.lst | coalg sat K' --warmup 1 --style basic --export-json metrics.json
hyperfine 'cat metric_formulas.lst | cool-coalg sat K' --warmup 1 --style basic --export-json metrics.json
python3 ./advanced_statistics.py metrics.json > metrics.txt
'';
......
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