Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

4 files changed, 85 insertions, 2 deletions

diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
new file mode 100644
index 0000000..9d3e999
--- /dev/null
+++ b/Assignment2/src/DTMC.dcl
@@ -0,0 +1,25 @@
+definition module DTMC
+
+from System.FilePath import :: FilePath
+
+:: DTMC =
+	{ nr_states :: !Int
+	, states    :: !{State}
+	}
+
+:: State =
+	{ actions  :: ![Action]
+	, init     :: !Bool
+	}
+
+:: Action =
+	{ action_id   :: !Int
+	, transitions :: ![Transition]
+	}
+
+:: Transition =
+	{ to_state    :: !Int
+	, probability :: !String
+	}
+
+parseDTMC :: !FilePath !*World -> *(!DTMC, !*World)
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
new file mode 100644
index 0000000..7c712e0
--- /dev/null
+++ b/Assignment2/src/DTMC.icl
@@ -0,0 +1,51 @@
+implementation module DTMC
+
+import StdArray
+import StdClass
+import StdFile
+import StdInt
+import StdList
+import StdString
+
+import Data.Error
+from Data.Func import $
+import System.File
+import System.FilePath
+import Text
+
+parseDTMC :: !FilePath !*World -> *(!DTMC, !*World)
+parseDTMC fp w
+# (lines,w) = readFileLines fp w
+= (parseDTMCFromLines [s % (0,size s-2) \\ s <- fromOk lines], w)
+
+parseDTMCFromLines :: ![String] -> DTMC
+parseDTMCFromLines lines
+# [nr_states:_:lines] = tl $ dropWhile ((<>) "@nr_states") lines
+# states = map parseState $ groupLines "\t" [] lines
+=
+	{ nr_states = toInt nr_states
+	, states    = {s \\ s <- states}
+	}
+where
+	parseState :: ![String] -> State
+	parseState [head:actions] =
+		{ actions = map parseAction $ groupLines "\t\t" [] actions
+		, init    = endsWith "init" head
+		}
+	where
+		parseAction :: ![String] -> Action
+		parseAction [head:transitions] =
+			{ action_id   = toInt (head % (8, size head-1))
+			, transitions = map parseTransition transitions
+			}
+		where
+			parseTransition :: !String -> Transition
+			parseTransition s = case split " : " (trim s) of
+				[id:prob:_] -> {to_state=toInt id, probability=prob}
+
+	groupLines :: !String ![String] ![String] -> [[String]]
+	groupLines head current [] = [reverse current]
+	groupLines head current [line:lines]
+	| startsWith head line = groupLines head [line:current] lines
+	| isEmpty current      = groupLines head [line] lines
+	| otherwise            = [reverse current:groupLines head [line] lines]
diff --git a/Assignment2/src/Dockerfile b/Assignment2/src/Dockerfile
index 03ff7ea..ecdbab0 100644
--- a/Assignment2/src/Dockerfile
+++ b/Assignment2/src/Dockerfile
@@ -16,5 +16,12 @@ RUN mkdir /opt/stormpy &&\
 	python3 setup.py build_ext --storm-dir /opt/storm/build develop &&\
 	py.test tests
 
-ENV PATH=$PATH:/opt/storm/build/bin
+RUN apt-get update -qq &&\
+	apt-get install -qq --no-install-recommends curl &&\
+	mkdir /opt/clean &&\
+	curl https://ftp.cs.ru.nl/Clean/builds/linux-x64/clean-bundle-complete-linux-x64-latest.tgz |\
+		tar xzv --strip-components=1 --directory=/opt/clean
+ENV CLEAN_HOME=/opt/clean
+
+ENV PATH=$PATH:/opt/storm/build/bin:/opt/clean/bin:/opt/clean/exe
 ENTRYPOINT cd /src; bash
diff --git a/Assignment2/src/start.sh b/Assignment2/src/start.sh
index aafbd9e..d07316f 100755
--- a/Assignment2/src/start.sh
+++ b/Assignment2/src/start.sh
@@ -2,7 +2,7 @@
 DOCKER_IMAGE=stormpy
 DOCKER_NAME=stormpy
 
-docker build -q -t $DOCKER_IMAGE .
+docker build -q -t $DOCKER_IMAGE . || exit
 
 docker run\
 	--mount type=bind,source="$PWD",target=/src\