From 418fc4e0dbc3ae276e398d6043f0f2b1213d78b2 Mon Sep 17 00:00:00 2001
From: xhajnal <matej.hajnal@gmail.com>
Date: Thu, 23 Jan 2020 16:18:35 +0100
Subject: [PATCH] adding examples

---
 .gitignore                          | 16 +++++++-----
 data/example/data_n=2.csv           |  2 ++
 models/example/semisynchronous_2.pm | 38 +++++++++++++++++++++++++++++
 properties/example/prop_2.pctl      |  3 +++
 4 files changed, 53 insertions(+), 6 deletions(-)
 create mode 100644 data/example/data_n=2.csv
 create mode 100644 models/example/semisynchronous_2.pm
 create mode 100644 properties/example/prop_2.pctl

diff --git a/.gitignore b/.gitignore
index d99c9a2..51ce072 100644
--- a/.gitignore
+++ b/.gitignore
@@ -113,7 +113,7 @@ venv.bak/
 \.DS_Store
 
 #########
-# Local #
+# LOCAL #
 #########
 ipython/*
 #!ipython/data*
@@ -121,11 +121,15 @@ ipython/*
 !ipython/*.md
 
 ./config.ini
+
 models/*
+!models/example/
+
 properties/*
+!properties/example/
 
-!data/*.p
-data/*/*
+data/*
+!data/example/
 
 results/data_intervals/*
 results/constraints/*
@@ -137,14 +141,14 @@ results/figures/*
 results/mh_results/*
 results/refinement_results/*
 
-
 src/test/*
 src/other_sources/*
 
-
 test/_trial_*
 
 tmp/*
 
-# storm calls
+###############
+# STORM CALLS #
+###############
 *.cmd
\ No newline at end of file
diff --git a/data/example/data_n=2.csv b/data/example/data_n=2.csv
new file mode 100644
index 0000000..e3802f4
--- /dev/null
+++ b/data/example/data_n=2.csv
@@ -0,0 +1,2 @@
+"n=2, p_v=0.81, q_v=0.92"
+0.04,0.02,0.94
diff --git a/models/example/semisynchronous_2.pm b/models/example/semisynchronous_2.pm
new file mode 100644
index 0000000..738d7ca
--- /dev/null
+++ b/models/example/semisynchronous_2.pm
@@ -0,0 +1,38 @@
+dtmc 
+ 
+const double p;
+const double q;
+
+module two_param_agents_2
+       // ai - state of agent i:  -1:init 0:total_failure 1:success 2:failure_after_first_attempt
+       a0 : [-1..2] init -1; 
+       a1 : [-1..2] init -1; 
+       b : [0..1] init 0; 
+
+       //  initial transition
+       []   a0 = -1 & a1 = -1 -> 1.0*p*p: (a0'=1) & (a1'=1) + 2.0*p*(1-p): (a0'=1) & (a1'=2) + 1.0*(1-p)*(1-p): (a0'=2) & (a1'=2);
+
+       // some ones, some zeros transitions
+       []   a0 = 0 & a1 = 0 -> (a0'= 0) & (a1'= 0) & (b'=1);
+       []   a0 = 1 & a1 = 0 -> (a0'= 1) & (a1'= 0) & (b'=1);
+       []   a0 = 1 & a1 = 1 -> (a0'= 1) & (a1'= 1) & (b'=1);
+
+       // some ones, some twos transitions
+       []   a0 = 1 & a1 = 2 -> q:(a0'= 1) & (a1'= 1) + 1-q:(a0'= 1) & (a1'= 0);
+
+       // some ones, some twos, some zeros transitions
+
+       // all twos transition
+       []   a0 = 2 & a1 = 2 -> (a0'= 0) & (a1'= 0);
+endmodule 
+
+rewards "mean" 
+       a0 = 0 & a1 = 0:0;
+       a0 = 1 & a1 = 0:1;
+       a0 = 1 & a1 = 1:2;
+endrewards 
+rewards "mean_squared" 
+       a0 = 0 & a1 = 0:0;
+       a0 = 1 & a1 = 0:1;
+       a0 = 1 & a1 = 1:4;
+endrewards 
diff --git a/properties/example/prop_2.pctl b/properties/example/prop_2.pctl
new file mode 100644
index 0000000..1d87e71
--- /dev/null
+++ b/properties/example/prop_2.pctl
@@ -0,0 +1,3 @@
+P=? [ F (a0=0)&(a1=0)&(b=1)]
+P=? [ F (a0=1)&(a1=0)&(b=1)]
+P=? [ F (a0=1)&(a1=1)&(b=1)]