diff options
Diffstat (limited to 'Assignment2/src/DTMC.icl')
| -rw-r--r-- | Assignment2/src/DTMC.icl | 38 |
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" |