diff --git a/prism-examples/molecules/knacl.csl b/prism-examples/molecules/knacl.csl index 4f589e77..0c84c189 100644 --- a/prism-examples/molecules/knacl.csl +++ b/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 ] diff --git a/prism-examples/molecules/knacl.sm b/prism-examples/molecules/knacl.sm index d2537be2..f0368880 100644 --- a/prism-examples/molecules/knacl.sm +++ b/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 diff --git a/prism-examples/molecules/mc.csl b/prism-examples/molecules/mc.csl index 304a6ed7..66ebb471 100644 --- a/prism-examples/molecules/mc.csl +++ b/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 ] diff --git a/prism-examples/molecules/mc.sm b/prism-examples/molecules/mc.sm index 61d47614..8f8c23d8 100644 --- a/prism-examples/molecules/mc.sm +++ b/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 diff --git a/prism-examples/molecules/nacl.csl b/prism-examples/molecules/nacl.csl index 754f62ad..15560fa9 100644 --- a/prism-examples/molecules/nacl.csl +++ b/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 ] diff --git a/prism-examples/molecules/nacl.sm b/prism-examples/molecules/nacl.sm index e2ac60d3..5a20f962 100644 --- a/prism-examples/molecules/nacl.sm +++ b/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