diff options
| author | Camil Staps | 2018-07-06 13:14:19 +0200 |
|---|---|---|
| committer | Camil Staps | 2018-07-06 13:14:19 +0200 |
| commit | 2b5ee228c3c77c077e42a7c82b0de9057b5e3a9a (patch) | |
| tree | 28417cef955739b45ebb6420c560b853ee4908e8 /Assignment2 | |
| parent | Remove redundant parentheses (diff) | |
| parent | Allow more powerfull properties by allowing operators (diff) | |
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment2')
| -rw-r--r-- | Assignment2/src/DTMC.dcl | 9 | ||||
| -rw-r--r-- | Assignment2/src/DTMC.icl | 12 |
2 files changed, 16 insertions, 5 deletions
diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl index b663431..e7d0a78 100644 --- a/Assignment2/src/DTMC.dcl +++ b/Assignment2/src/DTMC.dcl @@ -4,6 +4,8 @@ from Data.Map import :: Map from Data.Maybe import :: Maybe from System.FilePath import :: FilePath +from StdOverloaded import class toString + :: *DTMC = { nr_states :: !Int , parameters :: ![String] @@ -16,9 +18,12 @@ from System.FilePath import :: FilePath , init :: !Bool } +:: Op = LT | EQ | GT +instance toString Op + // Note that state_id must be an absorbing state -// (Probability, state_id) -:: Property :== (Real, Int) +// (Operator, Probability, state_id) +:: Property :== (Op, Real, Int) stateElimination :: !*DTMC -> *DTMC parseDTMC :: !FilePath !*World -> *(!*DTMC, !*World) diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl index 4bb6c18..53d1297 100644 --- a/Assignment2/src/DTMC.icl +++ b/Assignment2/src/DTMC.icl @@ -259,13 +259,19 @@ where | isJust state && (fromJust state).init = (fromJust state, states) | otherwise = findInitial` (i - 1) states +instance toString Op +where + toString LT = "<" + toString EQ = "=" + toString GT = ">" + assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World) -assertProperty (prob, target) dtmc z3 w +assertProperty (op, prob, target) dtmc z3 w # (init, dtmc) = findInitial dtmc # formula = 'M'.get target init.transitions | isNothing formula = abort "Cannot reach property target from initial state" # formula = fromJust formula -# formula = "(= " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")" +# formula = "( " <+ op <+ " " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")" # w = addAssert z3 formula w = (dtmc, w) @@ -301,4 +307,4 @@ Start w = w where prop :: Property - prop = (0.5, 7) // Chance to reach state 7 is 0.5 + prop = (EQ, 0.5, 7) // Chance to reach state 7 is 0.5 |