diff options
| author | Camil Staps | 2018-07-06 11:47:38 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-06 11:47:38 +0200 |
| commit | 9ffecd18ff061df9e7a52f09a0ea1610fda03c79 (patch) | |
| tree | 91b9a0a7e6cf1f527e699281ff653b19363e71a2 /Assignment2 | |
| parent | Fix compilation errors (diff) | |
Avoid beauty
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index c4e49c4..c532dfb 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -236,9 +236,8 @@ 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 = "((" <+ formula <+ ") = " <+ prob <+ ")" -# formula = parseInfix formula -# w = addAssert z3 (toString formula) w +# formula = "(= (" <+ prob <+ ") (" <+ parseInfix formula <+ "))" +# w = addAssert z3 formula w = (dtmc, w) Start w |