diff options
| -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 45abd4d..c89722b 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 <+ ") (" <+ parseInfix formula <+ "))" +# formula = "(" <+ op <+ " (" <+ prob <+ ") (" <+ parseInfix formula <+ "))" # w = addAssert z3 formula w = (dtmc, w) @@ -298,4 +304,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 |