molecules examples: fixed reward stuctures and properties

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@494 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism-examples/molecules/knacl.csl

@@ -1,15 +1,15 @@
 // Constants:
-const double T;
-const int i;
+const double T; // time instant
+const int i; // number of molecules
 
-// Probability of there being i Na molecules at time T?
+// Probability of there being i Na/K molecules at time T?
 P=? [ true U[T,T] na=i ]
-
-// Probability of there being i K molecules at time T?
 P=? [ true U[T,T] k=i ]
 
 // Expected percentage of Na/K molecules at time T?
-R=? [ I=T ]
+R{"percentage_na"}=? [ I=T ]
+R{"percentage_k"}=? [ I=T ]
 
 // Expected long-run percentage of Na/K molecules?
-R=? [ S ]
+R{"percentage_na"}=? [ S ]
+R{"percentage_k"}=? [ S ]

prism-examples/molecules/knacl.sm

@@ -5,9 +5,9 @@
 ctmc
 
 // constants
-const int N1 = 10; // number of Na molecules
-const int N2=N1; // number of Cl molecules
-const int N3=N1; // number of K molecules
+const int N1; // number of Na molecules
+const int N2; // number of Cl molecules
+const int N3; // number of K molecules
 
 // Na and Na+ module
 module na
@@ -70,15 +70,12 @@ module base_rates
 	
 endmodule
 
-// rewards (percentage of Na/K molecules)
-
-// set these variables equal to 0 or 1 depending on reward of interest
-const int na_reward;
-const int k_reward;
-
-rewards
-	
-	true : na_reward*100*na/N1;
-	true : k_reward*100*k/N3;
-	
+// reward structure (percentage of Na)
+rewards "percentage_na"
+	true : 100*na/N1;	
+endrewards
+
+// reward structure (percentage of K)
+rewards "percentage_k"
+	true : 100*k/N3;
 endrewards

prism-examples/molecules/mc.csl

@@ -1,18 +1,18 @@
 // Constants:
-const double T;
-const int i;
+const double T; // time instant
+const int i; // number of molecules
 
-// Probability of there being i Mg molecules at time T?
+// Probability of there being i Mg/Mg+/Mg+2 molecules at time T?
 P=? [ true U[T,T] mg=i ]
-
-// Probability of there being i Mg+ molecules at time T?
 P=? [ true U[T,T] mg_p=i ]
-
-// Probability of there being i Mg+2 molecules at time T?
 P=? [ true U[T,T] N1-(mg_p+mg)=i ]
 
 // Expected percentage of Mg/Mg+/Mg+2 molecules at time T?
-R=? [ I=T ]
+R{"percentage_mg"}=? [ I=T ]
+R{"percentage_mgplus"}=? [ I=T ]
+R{"percentage_mgplus2"}=? [ I=T ]
 
 // Expected long-run percentage of Mg/Mg+/Mg+2 molecules?
-R=? [ S ]
+R{"percentage_mg"}=? [ S ]
+R{"percentage_mgplus"}=? [ S ]
+R{"percentage_mgplus2"}=? [ S ]

prism-examples/molecules/mc.sm

@@ -5,8 +5,8 @@
 ctmc
 
 // constants
-const int N1 = 10; // number of Mg molecules
-const int N2 = N1; // number of Cl molecules
+const int N1; // number of Mg molecules
+const int N2; // number of Cl molecules
 
 
 // Cl and Cl- module
@@ -62,17 +62,17 @@ module base_rates
 	
 endmodule
 
-// rewards (percentage of Mg/Mg+/Mg+2 molecules)
+// reward structur: percentage of Mg molecules
+rewards "percentage_mg"
+	true : 100*mg/N1;
+endrewards
 
-// set these variables equal to 0 or 1 depending on reward of interest
-const int mg_reward;
-const int mgplus_reward;
-const int mgplus2_reward;
-
-rewards
-	
-	true : mg_reward*100*mg/N1;
-	true : mgplus_reward*100*mg_p/N1;
-	true : mgplus2_reward*max(100*(N1-(mg_p+mg))/N1,0);
-	
+// reward structur: percentage of Mg+ molecules
+rewards "percentage_mgplus"
+	true : 100*mg_p/N1;
+endrewards
+
+// reward structur: percentage of Mg+2 molecules
+rewards "percentage_mgplus2"
+	true : max(100*(N1-(mg_p+mg))/N1,0);
 endrewards

prism-examples/molecules/nacl.csl

@@ -1,6 +1,6 @@
 // Constants:
-const double T;
-const int i;
+const double T; // time instant
+const int i; // number of molecules
 
 // Probability of there being i Na molecules at time T?
 P=? [ true U[T,T] na=i ]

prism-examples/molecules/nacl.sm

@@ -5,8 +5,8 @@
 ctmc
 
 // constants
-const int N1 = 10; // number of Na molecules
-const int N2 = N1; // number of Cl molecules
+const int N1; // number of Na molecules
+const int N2; // number of Cl molecules
 
 // Na and Na+ module
 module na
@@ -47,8 +47,6 @@ module base_rates
 endmodule
 
 // rewards: "percentage of Na molecules present (out of all Na/Na+ molecules)"
-rewards
-	
+rewards "percentage_na"
 	true : 100*na/N1;
-	
 endrewards