diff --git a/examples/pdtmc/nand/nand_10-1.pm b/examples/pdtmc/nand/nand_10-1.pm index f56664199..b889db7e8 100644 --- a/examples/pdtmc/nand/nand_10-1.pm +++ b/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 diff --git a/examples/pdtmc/nand/nand_10-2.pm b/examples/pdtmc/nand/nand_10-2.pm index 0708144e7..43b3f54c1 100644 --- a/examples/pdtmc/nand/nand_10-2.pm +++ b/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 - diff --git a/examples/pdtmc/nand/nand_10-3.pm b/examples/pdtmc/nand/nand_10-3.pm index 566251af3..96f4568e4 100644 --- a/examples/pdtmc/nand/nand_10-3.pm +++ b/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 - diff --git a/examples/pdtmc/nand/nand_10-4.pm b/examples/pdtmc/nand/nand_10-4.pm index 7de796d1d..995e78f6b 100644 --- a/examples/pdtmc/nand/nand_10-4.pm +++ b/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 - diff --git a/examples/pdtmc/nand/nand_10-5.pm b/examples/pdtmc/nand/nand_10-5.pm index 2b1405c2f..5a1006a73 100644 --- a/examples/pdtmc/nand/nand_10-5.pm +++ b/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; diff --git a/examples/pdtmc/nand/nand_20-1.pm b/examples/pdtmc/nand/nand_20-1.pm index babaecbe3..fe8c89c3c 100644 --- a/examples/pdtmc/nand/nand_20-1.pm +++ b/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 - diff --git a/examples/pdtmc/nand/nand_20-2.pm b/examples/pdtmc/nand/nand_20-2.pm index 164a03e0f..29ecfe36d 100644 --- a/examples/pdtmc/nand/nand_20-2.pm +++ b/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 diff --git a/examples/pdtmc/nand/nand_20-3.pm b/examples/pdtmc/nand/nand_20-3.pm index 5131d1290..08662ea7f 100644 --- a/examples/pdtmc/nand/nand_20-3.pm +++ b/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 - diff --git a/examples/pdtmc/nand/nand_20-4.pm b/examples/pdtmc/nand/nand_20-4.pm index 047f8ac5e..edcf7b5c6 100644 --- a/examples/pdtmc/nand/nand_20-4.pm +++ b/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 diff --git a/examples/pdtmc/nand/nand_20-5.pm b/examples/pdtmc/nand/nand_20-5.pm index 2043bb018..2007fa413 100644 --- a/examples/pdtmc/nand/nand_20-5.pm +++ b/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 diff --git a/src/storage/parameters.h b/src/storage/parameters.h index 9dc862203..5313a0e23 100644 --- a/src/storage/parameters.h +++ b/src/storage/parameters.h @@ -13,9 +13,9 @@ namespace storm // typedef carl::MultivariatePolynomial Polynomial; typedef carl::Variable Variable; typedef carl::MultivariatePolynomial RawPolynomial; - typedef carl::FactorizedPolynomial Polynomial; +// typedef carl::FactorizedPolynomial Polynomial; -// typedef RawPolynomial Polynomial; + typedef RawPolynomial Polynomial; typedef carl::CompareRelation CompareRelation; typedef carl::RationalFunction RationalFunction;