From 98426aa139828e988b22c816e30ddfafad154b6c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 12 Mar 2013 13:19:14 +0100
Subject: [PATCH] Added new MDP example 'consensus'. Added some test checking
 to storm.cpp.

---
 examples/mdp/consensus/coin.pctl | 20 +++++++++
 src/storm.cpp                    | 70 ++++++++++++++++++++++++++++++++
 2 files changed, 90 insertions(+)
 create mode 100644 examples/mdp/consensus/coin.pctl

diff --git a/examples/mdp/consensus/coin.pctl b/examples/mdp/consensus/coin.pctl
new file mode 100644
index 000000000..52a308559
--- /dev/null
+++ b/examples/mdp/consensus/coin.pctl
@@ -0,0 +1,20 @@
+// C1 (with probability 1, all N processes finish the protocol)
+Pmin=? [ F "finished" ]
+
+// C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2)
+// Results are same for v=1 and v=2 by symmetry
+// Analytic bound is (K-1)/(2*K)
+Pmin=? [ F "finished"&"all_coins_equal_0" ]
+Pmin=? [ F "finished"&"all_coins_equal_1" ]
+
+// Max probability of finishing protocol with coins not all equal
+Pmax=? [ F "finished"&!"agree" ]
+
+// Min/max probability of finishing within k steps
+Pmin=? [ F<=k "finished" ]
+Pmax=? [ F<=k "finished" ]
+
+// Min/max expected steps to finish
+Rmin=? [ F "finished" ]
+Rmax=? [ F "finished" ]
+
diff --git a/src/storm.cpp b/src/storm.cpp
index 42de54751..6714e7930 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -360,6 +360,75 @@ void testCheckingAsynchLeader(storm::models::Mdp<double>& mdp) {
 	delete mc;
 }
 
+void testCheckingConsensus(storm::models::Mdp<double>& mdp) {
+	storm::formula::Ap<double>* finishedFormula = new storm::formula::Ap<double>("finished");
+	storm::formula::Eventually<double>* eventuallyFormula = new storm::formula::Eventually<double>(finishedFormula);
+	storm::formula::ProbabilisticNoBoundOperator<double>* probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	storm::modelChecker::GmmxxMdpPrctlModelChecker<double>* mc = new storm::modelChecker::GmmxxMdpPrctlModelChecker<double>(mdp);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	finishedFormula = new storm::formula::Ap<double>("finished");
+	storm::formula::Ap<double>* allCoinsEqual0Formula = new storm::formula::Ap<double>("all_coins_equal_0");
+	storm::formula::And<double>* conjunctionFormula = new storm::formula::And<double>(finishedFormula, allCoinsEqual0Formula);
+	eventuallyFormula = new storm::formula::Eventually<double>(conjunctionFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	finishedFormula = new storm::formula::Ap<double>("finished");
+	storm::formula::Ap<double>* allCoinsEqual1Formula = new storm::formula::Ap<double>("all_coins_equal_1");
+	conjunctionFormula = new storm::formula::And<double>(finishedFormula, allCoinsEqual1Formula);
+	eventuallyFormula = new storm::formula::Eventually<double>(conjunctionFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	finishedFormula = new storm::formula::Ap<double>("finished");
+	storm::formula::Ap<double>* agree = new storm::formula::Ap<double>("agree");
+	storm::formula::Not<double>* notAgree = new storm::formula::Not<double>(agree);
+	conjunctionFormula = new storm::formula::And<double>(finishedFormula, notAgree);
+	eventuallyFormula = new storm::formula::Eventually<double>(conjunctionFormula);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	finishedFormula = new storm::formula::Ap<double>("finished");
+	storm::formula::BoundedEventually<double>* boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(finishedFormula, 50);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	finishedFormula = new storm::formula::Ap<double>("finished");
+	boundedEventuallyFormula = new storm::formula::BoundedEventually<double>(finishedFormula, 50);
+	probFormula = new storm::formula::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
+
+	mc->check(*probFormula);
+	delete probFormula;
+
+	finishedFormula = new storm::formula::Ap<double>("finished");
+	storm::formula::ReachabilityReward<double>* reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(finishedFormula);
+	storm::formula::RewardNoBoundOperator<double>* rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
+
+	mc->check(*rewardFormula);
+	delete rewardFormula;
+
+	finishedFormula = new storm::formula::Ap<double>("finished");
+	reachabilityRewardFormula = new storm::formula::ReachabilityReward<double>(finishedFormula);
+	rewardFormula = new storm::formula::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
+
+	mc->check(*rewardFormula);
+	delete rewardFormula;
+
+	delete mc;
+}
+
 /*!
  * Simple testing procedure.
  */
@@ -380,6 +449,7 @@ void testChecking() {
 
 		// testCheckingDice(*mdp);
 		// testCheckingAsynchLeader(*mdp);
+		// testCheckingConsensus(*mdp);
 	} else {
 		std::cout << "Input is neither a DTMC nor an MDP." << std::endl;
 	}