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

1 files changed, 25 insertions, 0 deletions

diff --git a/Assignment2/src/README b/Assignment2/src/README
new file mode 100644
index 0000000..5fa6f9a
--- /dev/null
+++ b/Assignment2/src/README
@@ -0,0 +1,25 @@
+You can run this tool in Docker.
+All you need to do is run:
+
+	./start.sh die.prism die.properties
+
+Which repairs the model in die.prism for the properties in die.properties.
+
+The first time, this will build the Docker image. This can take a while, and
+may seem to freeze your system, and no progress is reported (unless you remove
+the -q switch in start.sh). The next time will be faster.
+
+The result is a Z3 model which contains instantiations for variables like v0x1.
+These are the values that should be added to the probabilities of transitions
+(here from state 0 to state 1) to make the model satisfy. Additionally, there
+is a variable cost which is the cost of the reparation. By default, this is the
+Sum of Squared Errors measure. To change to the Number of Modified Transitions
+measure, change line 328 of DTMC.icl to:
+
+	# (config,dtmc) = repairConfig NumberModifiedTransitions dtmc
+
+To run Z3 with a minimisation goal, uncomment line 339 in the same line.
+Additionally, to approximate the cost as described in the discussion of the
+paper, add a line like this under line 338:
+
+	# w = addAssert z3 "(> 0.3 cost)" w