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

5 files changed, 97 insertions, 223 deletions

diff --git a/.gitignore b/.gitignore
index 434aaf8..3a38369 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,229 +1,20 @@
-### LaTeX ###
-## Core latex/pdflatex auxiliary files:
 *.aux
-*.lof
-*.log
-*.lot
-*.fls
-*.out
-*.toc
-*.fmt
-*.fot
-*.cb
-*.cb2
-
-## Intermediate documents:
-*.dvi
-*.xdv
-*-converted-to.*
-*.ps
-*.eps
-*.pdf
-
-## Generated if empty string is given at "Please type another file name for output:"
-.pdf
-
-## Bibliography auxiliary files (bibtex/biblatex/biber):
 *.bbl
 *.bcf
 *.blg
-*-blx.aux
-*-blx.bib
-*.run.xml
-
-## Build tool auxiliary files:
+*.cb
+*.cb2
 *.fdb_latexmk
-*.synctex
-*.synctex(busy)
-*.synctex.gz
-*.synctex.gz(busy)
-*.pdfsync
-*Notes.bib
-
-## Auxiliary and intermediate files from other packages:
-# algorithms
-*.alg
-*.loa
-
-# achemso
-acs-*.bib
-
-# amsthm
-*.thm
-
-# beamer
-*.nav
-*.pre
-*.snm
-*.vrb
-
-# changes
-*.soc
-
-# cprotect
-*.cpt
-
-# elsarticle (documentclass of Elsevier journals)
-*.spl
-
-# endnotes
-*.ent
-
-# fixme
-*.lox
-
-# feynmf/feynmp
-*.mf
-*.mp
-*.t[1-9]
-*.t[1-9][0-9]
-*.tfm
-
-#(r)(e)ledmac/(r)(e)ledpar
-*.end
-*.?end
-*.[1-9]
-*.[1-9][0-9]
-*.[1-9][0-9][0-9]
-*.[1-9]R
-*.[1-9][0-9]R
-*.[1-9][0-9][0-9]R
-*.eledsec[1-9]
-*.eledsec[1-9]R
-*.eledsec[1-9][0-9]
-*.eledsec[1-9][0-9]R
-*.eledsec[1-9][0-9][0-9]
-*.eledsec[1-9][0-9][0-9]R
-
-# glossaries
-*.acn
-*.acr
-*.glg
-*.glo
-*.gls
-*.glsdefs
-
-# gnuplottex
-*-gnuplottex-*
-
-# gregoriotex
-*.gaux
-*.gtex
-
-# hyperref
-*.brf
-
-# knitr
-*-concordance.tex
-# TODO Comment the next line if you want to keep your tikz graphics files
-*.tikz
-*-tikzDictionary
-
-# listings
-*.lol
-
-# makeidx
-*.idx
-*.ilg
-*.ind
-*.ist
-
-# minitoc
-*.maf
-*.mlf
-*.mlt
-*.mtc[0-9]*
-*.slf[0-9]*
-*.slt[0-9]*
-*.stc[0-9]*
-
-# minted
-_minted*
-*.pyg
-
-# morewrites
-*.mw
-
-# nomencl
-*.nlo
-
-# pax
-*.pax
-
-# pdfpcnotes
-*.pdfpc
-
-# sagetex
-*.sagetex.sage
-*.sagetex.py
-*.sagetex.scmd
-
-# scrwfile
-*.wrt
-
-# sympy
-*.sout
-*.sympy
-sympy-plots-for-*.tex/
-
-# pdfcomment
-*.upa
-*.upb
-
-# pythontex
-*.pytxcode
-pythontex-files-*/
-
-# thmtools
-*.loe
-
-# TikZ & PGF
-*.dpth
-*.md5
-*.auxlock
-
-# todonotes
-*.tdo
-
-# easy-todo
-*.lod
-
-# xindy
-*.xdy
-
-# xypic precompiled matrices
-*.xyc
-
-# endfloat
-*.ttt
-*.fff
-
-# Latexian
-TSWLatexianTemp*
-
-## Editors:
-# WinEdt
-*.bak
-*.sav
-
-# Texpad
-.texpadtmp
-
-# Kile
-*.backup
-
-# KBibTeX
-*~[0-9]*
-
-# auto folder when using emacs and auctex
-/auto/*
-
-# expex forward references with \gathertags
-*-tags.tex
+*.fls
+*.fmt
+*.log
+*.out
+*.pdf
+*.run.xml
+*.toc
 
-### LaTeX Patch ###
-# glossaries
-*.glstex
+Clean System Files/
 
+__pycache__/
 
-# End of https://www.gitignore.io/api/latex
+*.drn
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\