diff options
| author | Camil Staps | 2018-07-06 11:45:12 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-06 11:45:12 +0200 |
| commit | a0e2b5b01800cd63596b37d4c02f15491384d825 (patch) | |
| tree | 1c1d80f2fbcf237fb53a025f6235a34ae586ebac /Assignment2 | |
| parent | Assert simple formula in z3 (diff) | |
Fix compilation errors
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index b2d88cf..c4e49c4 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -218,27 +218,27 @@ where addVar f t (Just fn) = Just ("((" <+ fn <+ ") + v" <+ f <+ "_" <+ t <+ ")") findInitial :: !*DTMC -> (!State, !*DTMC) -findInitial dtmc -# (states, dtmc) = dtmc!states -# (m, dtmc) = dtmc!nr_states -= findInitial` 0 m states +findInitial dtmc=:{nr_states,states} +# (init,states) = findInitial` (nr_states-1) states +# dtmc & states = states += (init, dtmc) where - findInitial` :: !Int !Int !*{Maybe State} -> State - findInitial` i m states - | i >= m = abort "No initial state" + findInitial` :: !Int !*{Maybe State} -> *(!State, !*{Maybe State}) + findInitial` i states + | i < 0 = abort "No initial state" # (state, states) = states![i] - | state.init = state - | otherwise = findInitial` (i + 1) m states + | isJust state && (fromJust state).init = (fromJust state, states) + | otherwise = findInitial` (i - 1) states assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World) assertProperty (prob, target) dtmc z3 w # (init, dtmc) = findInitial dtmc -# formula = M.get target init.transitions +# 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 -# (z3, w) = addAssert z3 (toString formula) w +# w = addAssert z3 (toString formula) w = (dtmc, w) Start w |