jani examples

Former-commit-id: 612da4705f

examples/jani-examples/beb.jani.txt

@@ -0,0 +1,27 @@
+Peak memory usage: 38 MB
+Analysis results for beb.jani
+
++ State space exploration
+  States:      4528
+  Transitions: 4874
+  Branches:    6899
+  Time:        0.0 s
+  Rate:        92408 states/s
+
++ LineSeized
+  Probability: 0.9166259765625
+  Time:        0.1 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  8
+    Time:        0.0 s
+
++ GaveUp
+  Probability: 0.0833740234375
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  9
+    Time:        0.0 s

examples/jani-examples/beb.modest

@@ -0,0 +1,64 @@
+// Modest MDP model of the bounded exponential backoff procedure (BEB)
+// [BFHH11]
+action tick, tack, tock;
+
+const int K = 4; // maximum value for backoff
+const int N = 3; // number of tries before giving up
+const int H = 3; // number of hosts (must correspond to the number of Host() instantiations in the global composition)
+
+int(0..2) cr; // count how many hosts attempt to seize the line in a slot (zero, one, many)
+bool line_seized;
+bool gave_up;
+
+property LineSeized = Pmax(<> line_seized); // some host managed to seize the line before any other gave up
+property GaveUp = Pmax(<> gave_up); // some host gave up before any other managed to seize the line (does not work with POR)
+
+process Clock()
+{
+	tick; tack; tau {= cr = 0 =}; tock; Clock()
+}
+
+process Host()
+{
+	int(0..N) na;     // nr_attempts 0..N
+	int(0..K) ev = 2; // exp_val 0..K
+	int(0..K) wt;     // slots_to_wait 0..K
+
+	do
+	{
+		if(wt > 0)
+		{
+			// wait this slot
+			tick {= wt-- =}
+		}
+		else
+		{
+			tau {= cr = min(2, cr + 1) =}; // attempt to seize the line
+			tick;
+			if(cr == 1)
+			{
+				// someone managed to seize the line
+				tau {= line_seized = true =}; stop
+			}
+			else if(na >= N)
+			{
+				// maximum number of attempts exceeded
+				tau {= gave_up = true =}; stop
+			}
+			else
+			{
+				// backoff
+				tau {= na++, wt = DiscreteUniform(0, max(0, ev - 1)), ev = min(2 * ev, K) =} 
+			}
+		};
+		tack; tock
+	}
+}
+
+par
+{
+::	Clock()
+::	Host()
+::	Host()
+::	Host()
+}

examples/jani-examples/beb.modest.txt

@@ -0,0 +1,27 @@
+Peak memory usage: 39 MB
+Analysis results for beb.modest
+
++ State space exploration
+  States:      4528
+  Transitions: 4874
+  Branches:    6899
+  Time:        0.0 s
+  Rate:        94333 states/s
+
++ LineSeized
+  Probability: 0.9166259765625
+  Time:        0.1 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  8
+    Time:        0.0 s
+
++ GaveUp
+  Probability: 0.0833740234375
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  9
+    Time:        0.0 s

examples/jani-examples/brp.jani.txt

@@ -0,0 +1,63 @@
+Peak memory usage: 39 MB
+Analysis results for brp.jani
+
++ State space exploration
+  States:      3959
+  Transitions: 4244
+  Branches:    4593
+  Time:        0.1 s
+  Rate:        74698 states/s
+
++ P_A
+  Probability: 0
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  1
+    Time:        0.0 s
+
++ P_B
+  Probability: 0
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  1
+    Time:        0.0 s
+
++ P_1
+  Probability: 0.000423333443357766
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 2.35005704803786E-07
+    Iterations:  13
+    Time:        0.0 s
+
++ P_2
+  Probability: 2.64530890961023E-05
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 2.05561452068843E-07
+    Iterations:  14
+    Time:        0.0 s
+
++ P_3
+  Probability: 0.000185191226393368
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 3.32462409056221E-07
+    Iterations:  13
+    Time:        0.0 s
+
++ P_4
+  Probability: 8E-06
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  2
+    Time:        0.0 s

examples/jani-examples/brp.modest

@@ -0,0 +1,213 @@
+// Modest PTA model of the bounded retransmission protocol (BRP)
+// [HH09], http://www.modestchecker.net/CaseStudies/BRP/
+action put, get, put_k, get_k, put_l, get_l;
+action new_file;
+action s_ok, s_dk, s_nok, s_restart;
+action r_ok, r_inc, r_fst, r_nok, r_timeout;
+exception error;
+
+const int N = 16; // number of frames per file
+const int MAX = 2; // maximum number of retransmissions per frame
+const int TD = 1; // transmission delay
+const int TS = 2 * TD + 1; // sender timeout
+const int TR = 2 * MAX * TS + 3 * TD; // receiver timeout
+const int SYNC = TR;
+
+bool ff, lf, ab; // channel data: first/last frame, alternating bit
+int(0..N) i; // sender chunk counter
+bool inTransitK = false;
+bool inTransitL = false;
+
+bool first_file_done = false;
+bool get_k_seen, s_ok_seen, s_nok_seen, s_dk_seen, s_restart_seen, r_ok_seen, r_timeout_seen;
+
+// Invariant (timed) properties (from [BrpOnTime], the TA model)
+bool premature_timeout, channel_k_overflow, channel_l_overflow;
+// "there is at most one message in transit for each channel"
+property T_1 = A[] (!(channel_k_overflow || channel_l_overflow));
+// "there is at most one message in transit in total"
+property T_2 = A[] (!(inTransitK && inTransitL));
+// Assumption (A1): "no premature timeouts"
+property T_A1 = A[] (!premature_timeout);
+// Assumption (A2): "sender starts new file only after receiver reacted to failure"
+// Note that receiver can only notice failure if it received at least one chunk, i.e. get_k_seen
+property T_A2 = A[] (!s_restart_seen || !get_k_seen || r_timeout_seen);
+
+// Probabilistic reachability properties (from [D'AJJL01], the RAPTURE/PRISM model)
+// property A of [D'AJJL01]: "the maximum probability that eventually the sender reports 
+// a certain unsuccessful transmission but the receiver got the complete file"
+property P_A = Pmax(<>(s_nok_seen && r_ok_seen));
+// property B of [D'AJJL01]: "the maximum probability that eventually the sender reports
+// a certain successful transmission but the receiver did not get the complete file"
+property P_B = Pmax(<>(s_ok_seen && !r_ok_seen));
+// property 1 of [D'AJJL01]: "the maximum probability that eventually the sender
+// does not report a successful transmission"
+property P_1 = Pmax(<>(s_nok_seen || s_dk_seen));
+// property 2 of [D'AJJL01]: "the maximum probability that eventually the sender
+// reports an uncertainty on the success of the transmission"
+property P_2 = Pmax(<>(s_dk_seen));
+// property 3 of [D'AJJL01]: "the maximum probability that eventually the sender
+// reports an unsuccessful transmission after more than 8 chunks have been sent successfully"
+property P_3 = Pmax(<>(s_nok_seen && i > 8));
+// property 4 of [D'AJJL01]: "the maximum probability that eventually the receiver
+// does not receive any chunk and the sender tried to send a chunk"
+property P_4 = Pmax(<>((s_ok_seen || s_nok_seen || s_dk_seen) && !get_k_seen));
+
+
+process Sender()
+{
+	bool bit;
+	int(0..MAX) rc;
+	clock c;
+
+	try
+	{
+		do {
+		::	when urgent(i < N) {= i++ =};
+			do
+			{
+				// send frame
+				invariant(c <= 0) put_k {= ff = (i == 1), lf = (i == N), ab = bit, c = 0 =};
+				invariant(c <= TS) alt {
+				::	// receive ack
+					get_l {= bit = !bit, rc = 0, c = 0 =};
+					urgent break
+				:: // timeout
+					when(c >= TS)
+					if(rc < MAX)
+					{
+						// retry
+						{= rc++, c = 0 =}
+					}
+					else if(i < N)
+					{
+						// no retries left
+						s_nok {= rc = 0, c = 0 =};
+						urgent throw(error)
+					}
+					else
+					{
+						// no retries left
+						s_dk {= rc = 0, c = 0 =};
+						urgent throw(error)
+					}
+				}
+			}
+		::	when(i == N)
+			// file transmission successfully completed
+			invariant(c <= 0) s_ok {= first_file_done = true =};
+			urgent break
+		}
+	}
+	catch error
+	{
+		// File transfer did not succeed: wait, then restart with next file
+		invariant(c <= SYNC) when(c >= SYNC)
+		s_restart {= bit = false, first_file_done = true =}
+	}
+}
+
+process Receiver()
+{
+	bool r_ff, r_lf, r_ab;
+	bool bit;
+	clock c;
+
+	// receive first frame
+	if(ff) { get_k {= c = 0, bit = ab, r_ff = ff, r_lf = lf, r_ab = ab =} }
+	else { get_k {= c = 0, premature_timeout = true =}; stop };
+	do
+	{
+		invariant(c <= 0)
+		{
+			if(r_ab != bit)
+			{
+				// repetition, re-ack
+				put_l
+			}
+			else
+			{
+				// report frame
+				if(r_lf)      { r_ok }
+				else if(r_ff) { r_fst }
+				else          { r_inc };
+				put_l {= bit = !bit =}
+			}
+		};
+		invariant(c <= TR)
+		{
+			alt {
+			::	// receive next frame
+				get_k {= c = 0, r_ff = ff, r_lf = lf, r_ab = ab =}
+			::	// timeout
+				when(c == TR)
+				if(r_lf)
+				{
+					// we just got the last frame, though
+					r_timeout; break
+				}
+				else
+				{
+					r_nok;
+					// abort transfer
+					r_timeout; break
+				}
+			}
+		}
+	};
+	Receiver()
+}
+
+process ChannelK()
+{
+	clock c;
+
+	put_k palt
+	{
+		:98:	{= c = 0, inTransitK = true =};
+				invariant(c <= TD) alt {
+				::	get_k {= inTransitK = false =}
+				::	put_k {= channel_k_overflow = true =}; stop
+				}
+		: 2:	{==}
+	};
+	ChannelK()
+}
+
+process ChannelL()
+{
+	clock c;
+
+	put_l palt
+	{
+		:99:	{= c = 0, inTransitL = true =};
+				invariant(c <= TD) alt {
+				::	get_l {= inTransitL = false =}
+				::	put_l {= channel_l_overflow = true =}; stop
+				}
+		: 1:	{==}
+	};
+	ChannelL()
+}
+
+process Observer()
+{
+	alt {
+	::	get_k     {= get_k_seen     = true =}
+	::	s_ok      {= s_ok_seen      = true =}
+	::	s_nok     {= s_nok_seen     = true =}
+	::	s_dk      {= s_dk_seen      = true =}
+	::	s_restart {= s_restart_seen = true =}
+	::	r_ok      {= r_ok_seen      = true =}
+	::	r_timeout {= r_timeout_seen = true =}
+	};
+	Observer()
+}
+
+par {
+::	Sender()
+::	Receiver()
+::	ChannelK()
+::	ChannelL()
+::	Observer()
+}

examples/jani-examples/brp.modest.txt

@@ -0,0 +1,63 @@
+Peak memory usage: 40 MB
+Analysis results for brp.modest
+
++ State space exploration
+  States:      3959
+  Transitions: 4244
+  Branches:    4593
+  Time:        0.1 s
+  Rate:        73315 states/s
+
++ P_A
+  Probability: 0
+  Time:        0.1 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  1
+    Time:        0.0 s
+
++ P_B
+  Probability: 0
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  1
+    Time:        0.0 s
+
++ P_1
+  Probability: 0.000423333443357766
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 2.35005704803786E-07
+    Iterations:  13
+    Time:        0.0 s
+
++ P_2
+  Probability: 2.64530890961023E-05
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 2.05561452068843E-07
+    Iterations:  14
+    Time:        0.0 s
+
++ P_3
+  Probability: 0.000185191226393368
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 3.32462409056221E-07
+    Iterations:  13
+    Time:        0.0 s
+
++ P_4
+  Probability: 8E-06
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 0
+    Iterations:  2
+    Time:        0.0 s

examples/jani-examples/consensus-6.jani.txt

@@ -0,0 +1,27 @@
+Peak memory usage: 530 MB
+Analysis results for consensus-6.jani
+
++ State space exploration
+  States:      2345194
+  Transitions: 9418584
+  Branches:    13891248
+  Time:        8.7 s
+  Rate:        270964 states/s
+
++ C1
+  Result:                       True
+  Time for min. prob. 0 states: 1.6 s
+  Time for min. prob. 1 states: 0.1 s
+  Time:                         1.7 s
+  Min. probability:             1
+
++ C2
+  Probability:                  0.395776147642961
+  Time for min. prob. 0 states: 2.0 s
+  Time for min. prob. 1 states: 0.1 s
+  Time:                         125.8 s
+
+  + Value iteration
+    Final error: 9.96634356860147E-07
+    Iterations:  2137
+    Time:        123.8 s

examples/jani-examples/consensus-6.modest

@@ -0,0 +1,157 @@
+// Modest version of http://www.prismmodelchecker.org/casestudies/consensus_prism.php
+// Command line: mcsta.exe consensus-6.modest -S Memory --nochainopt --bounded-alg StateElimination -E "K=2"
+
+action done;
+
+// constants
+const int N = 6;
+const int K = 4;
+const int range = 2 * (K + 1) * N;
+const int counter_init = (K + 1) * N;
+const int left = N;
+const int right = 2 * (K + 1) * N - N;
+
+// shared coin
+int(0..range) counter = counter_init;
+reward coin_flips;
+
+property C1 = P(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1)) >= 1;
+property C2 = Pmin(<> (fin1 == 1 && fin2 == 1 && fin3 == 1 && fin4 == 1 && fin5 == 1 && fin6 == 1 && coin1 == 1 && coin2 == 1 && coin3 == 1 && coin4 == 1 && coin5 == 1 && coin6 == 1));
+
+int(0..1) fin1, fin2, fin3, fin4, fin5, fin6;
+int(0..1) coin1, coin2, coin3, coin4, coin5, coin6;
+
+process Tourist1()
+{
+	process Flip() { palt { :1: {= coin1 = 0, coin_flips++ =} :1: {= coin1 = 1, coin_flips++ =} }; Write() }
+	process Write() {
+		alt {
+		::	when(coin1 == 0 && counter > 0) {= counter-- =}; Check()
+		::	when(coin1 == 1 && counter < range) {= counter++, coin1 = 0 =}; Check()
+		}
+	}
+	process Check() {
+		alt {
+		::	when(counter <= left) {= coin1 = 0, fin1 = 1 =}; Finished()
+		::	when(counter >= right) {= coin1 = 1, fin1 = 1 =}; Finished()
+		::	when(counter > left && counter < right) Tourist1()
+		}
+	}
+	process Finished() { done; Finished() }
+
+	Flip()
+}
+
+process Tourist2()
+{
+	process Flip() { palt { :1: {= coin2 = 0, coin_flips++ =} :1: {= coin2 = 1, coin_flips++ =} }; Write() }
+	process Write() {
+		alt {
+		::	when(coin2 == 0 && counter > 0) {= counter-- =}; Check()
+		::	when(coin2 == 1 && counter < range) {= counter++, coin2 = 0 =}; Check()
+		}
+	}
+	process Check() {
+		alt {
+		::	when(counter <= left) {= coin2 = 0, fin2 = 1 =}; Finished()
+		::	when(counter >= right) {= coin2 = 1, fin2 = 1 =}; Finished()
+		::	when(counter > left && counter < right) Tourist2()
+		}
+	}
+	process Finished() { done; Finished() }
+
+	Flip()
+}
+
+process Tourist3()
+{
+	process Flip() { palt { :1: {= coin3 = 0, coin_flips++ =} :1: {= coin3 = 1, coin_flips++ =} }; Write() }
+	process Write() {
+		alt {
+		::	when(coin3 == 0 && counter > 0) {= counter-- =}; Check()
+		::	when(coin3 == 1 && counter < range) {= counter++, coin3 = 0 =}; Check()
+		}
+	}
+	process Check() {
+		alt {
+		::	when(counter <= left) {= coin3 = 0, fin3 = 1 =}; Finished()
+		::	when(counter >= right) {= coin3 = 1, fin3 = 1 =}; Finished()
+		::	when(counter > left && counter < right) Tourist3()
+		}
+	}
+	process Finished() { done; Finished() }
+
+	Flip()
+}
+
+process Tourist4()
+{
+	process Flip() { palt { :1: {= coin4 = 0, coin_flips++ =} :1: {= coin4 = 1, coin_flips++ =} }; Write() }
+	process Write() {
+		alt {
+		::	when(coin4 == 0 && counter > 0) {= counter-- =}; Check()
+		::	when(coin4 == 1 && counter < range) {= counter++, coin4 = 0 =}; Check()
+		}
+	}
+	process Check() {
+		alt {
+		::	when(counter <= left) {= coin4 = 0, fin4 = 1 =}; Finished()
+		::	when(counter >= right) {= coin4 = 1, fin4 = 1 =}; Finished()
+		::	when(counter > left && counter < right) Tourist4()
+		}
+	}
+	process Finished() { done; Finished() }
+
+	Flip()
+}
+
+process Tourist5()
+{
+	process Flip() { palt { :1: {= coin5 = 0, coin_flips++ =} :1: {= coin5 = 1, coin_flips++ =} }; Write() }
+	process Write() {
+		alt {
+		::	when(coin5 == 0 && counter > 0) {= counter-- =}; Check()
+		::	when(coin5 == 1 && counter < range) {= counter++, coin5 = 0 =}; Check()
+		}
+	}
+	process Check() {
+		alt {
+		::	when(counter <= left) {= coin5 = 0, fin5 = 1 =}; Finished()
+		::	when(counter >= right) {= coin5 = 1, fin5 = 1 =}; Finished()
+		::	when(counter > left && counter < right) Tourist5()
+		}
+	}
+	process Finished() { done; Finished() }
+
+	Flip()
+}
+
+process Tourist6()
+{
+	process Flip() { palt { :1: {= coin6 = 0, coin_flips++ =} :1: {= coin6 = 1, coin_flips++ =} }; Write() }
+	process Write() {
+		alt {
+		::	when(coin6 == 0 && counter > 0) {= counter-- =}; Check()
+		::	when(coin6 == 1 && counter < range) {= counter++, coin6 = 0 =}; Check()
+		}
+	}
+	process Check() {
+		alt {
+		::	when(counter <= left) {= coin6 = 0, fin6 = 1 =}; Finished()
+		::	when(counter >= right) {= coin6 = 1, fin6 = 1 =}; Finished()
+		::	when(counter > left && counter < right)  Tourist6()
+		}
+	}
+	process Finished() { done; Finished() }
+
+	Flip()
+}
+
+par {
+::	Tourist1()
+::	Tourist2()
+::	Tourist3()
+::	Tourist4()
+::	Tourist5()
+::	Tourist6()
+}

examples/jani-examples/consensus-6.modest.txt

@@ -0,0 +1,27 @@
+Peak memory usage: 531 MB
+Analysis results for consensus-6.modest
+
++ State space exploration
+  States:      2345194
+  Transitions: 9418584
+  Branches:    13891248
+  Time:        8.2 s
+  Rate:        287507 states/s
+
++ C1
+  Result:                       True
+  Time for min. prob. 0 states: 1.5 s
+  Time for min. prob. 1 states: 0.2 s
+  Time:                         1.7 s
+  Min. probability:             1
+
++ C2
+  Probability:                  0.395776147642961
+  Time for min. prob. 0 states: 2.0 s
+  Time for min. prob. 1 states: 0.1 s
+  Time:                         126.8 s
+
+  + Value iteration
+    Final error: 9.96634356860147E-07
+    Iterations:  2137
+    Time:        124.7 s

examples/jani-examples/dice.jani

@@ -0,0 +1,354 @@
+{
+	"jani-version": 1,
+  "name": "dice",
+	"type" : "mdp",
+	"actions" : [],
+	"variables" : [
+		{
+			"name": "thrownSix",
+			"type": "bool",
+			"initial-value": false
+		},
+		{
+			"name": "terminated",
+			"type": "bool",
+			"initial-value": false
+		}
+	],
+	"rewards" : [
+		{
+			"name" : "step"
+		}
+	],
+	"properties" : [
+		{
+			"name" : "ProbThrowSix",
+			"reach" : "thrownSix",
+			"type": "probability-max-query"
+		},
+		{
+			"name" : "StepsUntilReach",
+			"reach" : "terminated",
+			"reward": "step",
+			"type": "expected-reachability-reward-max-query"
+		}
+	],
+	"automata" : [
+		{
+			"name" : "dice",
+			"variables" : [
+				{
+					"name" : "d",
+					"type" : {
+						"kind": "bounded",
+						"base": "int",
+						"lower-bound" : 0,
+						"upper-bound" : 6
+					},
+					"initial-value" : 0
+				}
+			],
+			"locations" : [
+				{
+					"name" : "s0"
+				},
+				{
+					"name" : "s1"
+				},
+				{
+					"name" : "s2"
+				},
+				{
+					"name" : "s3"
+				},
+				{
+					"name" : "s4"
+				},
+				{
+					"name" : "s5"
+				},
+				{
+					"name" : "s6"
+				},
+				{
+					"name" : "s7"
+				}
+			],
+			"initial-location" : "s0",
+			"edges" : [
+				{
+					"location" : "s0",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 0.5,
+							"location" : "s1",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						},
+						{
+							"probability" : 0.5,
+							"location" : "s2",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				},
+				{
+					"location" : "s1",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 0.5,
+							"location" : "s3",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						},
+						{
+							"probability" : 0.5,
+							"location" : "s4",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				},
+				{
+					"location" : "s2",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 0.5,
+							"location" : "s5",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						},
+						{
+							"probability" : 0.5,
+							"location" : "s6",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				},
+				{
+					"location" : "s3",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 0.5,
+							"location" : "s1",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						},
+						{
+							"probability" : 0.5,
+							"location" : "s7",
+							"assignments" : [
+								{
+									"ref" : "d",
+									"value" : 1
+								},
+								{
+									"ref" : "terminated",
+									"value" : true
+								}
+							],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				},
+				{
+					"location" : "s4",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 0.5,
+							"location" : "s7",
+							"assignments" : [
+								{
+									"ref" : "d",
+									"value" : 2
+								},
+								{
+									"ref" : "terminated",
+									"value" : true
+								}
+							],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						},
+						{
+							"probability" : 0.5,
+							"location" : "s7",
+							"assignments" : [
+								{
+									"ref" : "d",
+									"value" : 3
+								},
+								{
+									"ref" : "terminated",
+									"value" : true
+								}
+							],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				},
+				{
+					"location" : "s5",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 0.5,
+							"location" : "s7",
+							"assignments" : [
+								{
+									"ref" : "d",
+									"value" : 4
+								},
+								{
+									"ref" : "terminated",
+									"value" : true
+								}
+							],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						},
+						{
+							"probability" : 0.5,
+							"location" : "s7",
+							"assignments" : [
+								{
+									"ref" : "d",
+									"value" : 5
+								},
+								{
+									"ref" : "terminated",
+									"value" : true
+								}
+							],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				},
+				{
+					"location" : "s6",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 0.5,
+							"location" : "s2",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						},
+						{
+							"probability" : 0.5,
+							"location" : "s7",
+							"assignments" : [
+								{
+									"ref" : "d",
+									"value" : 6
+								},
+								{
+									"ref" : "thrownSix",
+									"value" : true
+								},
+								{
+									"ref" : "terminated",
+									"value" : true
+								}
+							],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				},
+				{
+					"location" : "s7",
+					"guard" : true,
+					"destinations" : [
+						{
+							"probability" : 1,
+							"location" : "s7",
+							"assignments" : [],
+							"rewards" : [
+								{
+									"ref" : "step",
+									"value" : 1
+								}
+							]
+						}
+					]
+				}
+			]
+		}
+	],
+	"system" : "dice"
+}

examples/jani-examples/dice.jani.txt

@@ -0,0 +1,29 @@
+Peak memory usage: 36 MB
+Analysis results for dice.jani
+
++ State space exploration
+  States:      8
+  Transitions: 8
+  Branches:    14
+  Time:        0.0 s
+  Rate:        190 states/s
+
++ ProbThrowSix
+  Probability: 0.166666626930237
+  Time:        0.0 s
+
+  + Value iteration
+    Final error: 7.15255907834985E-07
+    Iterations:  11
+    Time:        0.0 s
+
++ StepsUntilReach
+  Value:                        3.66666650772095
+  Time for min. prob. 0 states: 0.0 s
+  Time for min. prob. 1 states: 0.0 s
+  Time:                         0.0 s
+
+  + Value iteration
+    Final error: 4.08717619857464E-07
+    Iterations:  12
+    Time:        0.0 s