adding examples

.gitignore

@@ -113,19 +113,23 @@ venv.bak/
 \.DS_Store
 
 #########
-# Local #
+# LOCAL #
 #########
 ipython/*
 #!ipython/data*
 !ipython/*.ipynb
 !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

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

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 

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)]