diff options
Diffstat (limited to 'Assignment2/src/DTMC.icl')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index 45abd4d..4bb6c18 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) <+ ")" @@ -265,7 +265,7 @@ assertProperty (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 = "(= (" <+ prob <+ ") (" <+ parseInfix formula <+ "))" +# formula = "(= " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")" # w = addAssert z3 formula w = (dtmc, w) @@ -275,6 +275,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 |