summaryrefslogtreecommitdiff
path: root/Assignment2/src/DTMC.icl
diff options
context:
space:
mode:
Diffstat (limited to 'Assignment2/src/DTMC.icl')
-rw-r--r--Assignment2/src/DTMC.icl38
1 files changed, 20 insertions, 18 deletions
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 29b505c..83c5ac1 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -21,10 +21,13 @@ import System.CommandLine
import System.File
import System.FilePath
import Text
+import Text.GenParse
import Expression
import Z3
+derive gParse Op, (,,)
+
paths :: !*DTMC -> *([[Int]], !*DTMC)
paths dtmc=:{nr_states,states}
# (inits,states) = getInitStates (nr_states-1) states
@@ -275,7 +278,7 @@ assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World)
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"
+| isNothing formula = abort "Cannot reach property target from initial state\n"
# formula = fromJust formula
# formula = "( " <+ op <+ " " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")"
# w = addAssert z3 formula w
@@ -290,30 +293,29 @@ z3AddVars dtmc z3 w
parenthesise :: !a -> String | toString a
parenthesise x = let s = toString x in if (s.[0] == '(') s ("(" +++ s +++ ")")
+parseProperty :: !String -> Property
+parseProperty s = case parseString s of
+ Nothing -> abort $ "Could not parse '" +++ s +++ "' as a property\n"
+ Just p -> p
+
Start w
# ([prog:args],w) = getCommandLine w
-| length args <> 2
- # (io,w) = stdio w
- # io = io <<< "Usage: " <<< prog <<< " DRN_IN DRN_OUT\n"
- # (_,w) = fclose io w
- = ("", w)
-# [drn_in,drn_out:_] = args
+| length args <> 2 = "Usage: " +++ prog +++ " DRN PROPERTIES"
+# [drn_in,props:_] = args
+
# (dtmc,w) = parseDTMC drn_in w
+# (props,w) = readFileLines props w
+# props = map (parseProperty o trim) $ fromOk props
+
# dtmc = addVars dtmc
# dtmc = stateElimination dtmc
# (z3,w) = startZ3 w
# (dtmc,w) = z3AddVars dtmc z3 w
-# (dtmc,w) = assertProperties properties dtmc z3 w
+# (dtmc,w) = assertProperties props dtmc z3 w
# (rC,dtmc) = repairConfig dtmc
# w = seqSt (addAssert z3) rC.totality_restrictions w
-# (dtmcs,dtmc) = printDTMC dtmc
-# (_,w) = writeFile drn_out dtmcs w
# (sat,w) = checkSat z3 w
-| sat = getModel z3 w
-| otherwise = ("Could not satisfy the property", w)
-where
- properties :: Properties
- properties = [prop]
-
- prop :: Property
- prop = (EQ, 0.5, 7) // Chance to reach state 7 is 0.5
+| sat
+ # (model,w) = getModel z3 w
+ = model
+| otherwise = "Could not satisfy the property"