diff options
| author | Erin van der Veen | 2018-07-06 13:16:04 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-07-06 13:16:04 +0200 |
| commit | fda2da913385917c38322761eed3e22230cff153 (patch) | |
| tree | 4b56d0659a51f55d040a14e13d511a794979ee43 /Assignment2 | |
| parent | Allow multiple properties (diff) | |
| parent | Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking (diff) | |
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 7 | ||||
| -rw-r--r-- | Assignment2/src/Z3.icl | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index b1a12ce..0c71420 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -242,7 +242,7 @@ where = ([s:rest],ss) totality :: !State -> String - totality s = "(= 1 (" <+ parseInfix expr <+ "))" + totality s = "(= 1 " <+ parenthesise (parseInfix expr) <+ ")" where expr = "(" <+ (join ")+(" $ 'M'.elems s.transitions) <+ ")" @@ -277,7 +277,7 @@ assertProperty (op, prob, target) dtmc z3 w # formula = 'M'.get target init.transitions | isNothing formula = abort "Cannot reach property target from initial state" # formula = fromJust formula -# formula = "(" <+ op <+ " (" <+ prob <+ ") (" <+ parseInfix formula <+ "))" +# formula = "( " <+ op <+ " " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")" # w = addAssert z3 formula w = (dtmc, w) @@ -287,6 +287,9 @@ z3AddVars dtmc z3 w # w = seqSt (addVariable z3) param w = (dtmc,w) +parenthesise :: !a -> String | toString a +parenthesise x = let s = toString x in if (s.[0] == '(') s ("(" +++ s +++ ")") + Start w # ([prog:args],w) = getCommandLine w | length args <> 2 diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl index 2efe664..cb054e1 100644 --- a/Assignment2/src/Z3.icl +++ b/Assignment2/src/Z3.icl @@ -53,4 +53,4 @@ getModel z3 w = (out, w) trace_s :: String -> String -trace_s s = trace_n s s +trace_s s = trace s s |