diff options
| author | Camil Staps | 2018-07-06 13:13:28 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-06 13:13:28 +0200 |
| commit | 0ca046677c3a4051e25434258ed9b077400107dc (patch) | |
| tree | 4aea3e3ee938e76455d8c4ea17624cd23c24719a /Assignment2 | |
| parent | Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking (diff) | |
Remove redundant parentheses
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 7 | ||||
| -rw-r--r-- | Assignment2/src/Z3.dcl | 4 | ||||
| -rw-r--r-- | Assignment2/src/Z3.icl | 2 |
3 files changed, 8 insertions, 5 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 diff --git a/Assignment2/src/Z3.dcl b/Assignment2/src/Z3.dcl index e7555cf..8628d5d 100644 --- a/Assignment2/src/Z3.dcl +++ b/Assignment2/src/Z3.dcl @@ -5,8 +5,8 @@ from System.Process import :: ProcessHandle, :: ProcessIO :: Z3 startZ3 :: !*World -> (!Z3, !*World) -addAssert :: !Z3 !String !*World -> !*World -addVariable :: !Z3 !String !*World -> !*World +addAssert :: !Z3 !String !*World -> *World +addVariable :: !Z3 !String !*World -> *World checkSat :: !Z3 !*World -> (!Bool, !*World) // Note: getModel terminates z3 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 |