Adapted parameterized NAND example to use state rewards instead of transition rewards. Also, the unfactorized polynomials are now used to build and compute everything. We should detect cyclic models and use the factorized polynomials for them.

Former-commit-id: c4179f2029

examples/pdtmc/nand/nand_10-1.pm

@@ -67,9 +67,11 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-    [] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
 

examples/pdtmc/nand/nand_10-2.pm

@@ -67,9 +67,10 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
-

examples/pdtmc/nand/nand_10-3.pm

@@ -67,9 +67,10 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
-

examples/pdtmc/nand/nand_10-4.pm

@@ -67,9 +67,10 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
-

examples/pdtmc/nand/nand_10-5.pm

@@ -67,9 +67,5 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
-
-// rewards: final value of gate
-rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
-endrewards
+label "end" = s=4;
 

examples/pdtmc/nand/nand_20-1.pm

@@ -67,9 +67,10 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
-

examples/pdtmc/nand/nand_20-2.pm

@@ -67,9 +67,11 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
 

examples/pdtmc/nand/nand_20-3.pm

@@ -67,9 +67,10 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
-

examples/pdtmc/nand/nand_20-4.pm

@@ -67,9 +67,11 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
 

examples/pdtmc/nand/nand_20-5.pm

@@ -67,9 +67,11 @@ module multiplex
 endmodule
 
 label "target" = s=4 & z/N<0.1;
+label "end" = s=4;
 
 // rewards: final value of gate
 rewards
-	[] s=0 & (c=N) & (u=M) : z/N;
+    // [] s=0 & (c=N) & (u=M) : z/N;
+    s=0 & (c=N) & (u=M) : z/N;
 endrewards
 

src/storage/parameters.h

@@ -13,9 +13,9 @@ namespace storm
 //	typedef carl::MultivariatePolynomial<cln::cl_RA> Polynomial;
 	typedef carl::Variable  Variable;
     typedef carl::MultivariatePolynomial<cln::cl_RA> RawPolynomial;
-    typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
+//    typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
 
-//    typedef RawPolynomial Polynomial;
+    typedef RawPolynomial Polynomial;
 	
 	typedef carl::CompareRelation CompareRelation;
 	typedef carl::RationalFunction<Polynomial> RationalFunction;