From 61e78f8d120acb51fdec5ccf86aaf8b52dca69b0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Nov 2014 14:20:20 +0100 Subject: [PATCH] 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: c4179f20297f2e24ced4f06e1771055949979db0 --- examples/pdtmc/nand/nand_10-1.pm | 4 +++- examples/pdtmc/nand/nand_10-2.pm | 5 +++-- examples/pdtmc/nand/nand_10-3.pm | 5 +++-- examples/pdtmc/nand/nand_10-4.pm | 5 +++-- examples/pdtmc/nand/nand_10-5.pm | 6 +----- examples/pdtmc/nand/nand_20-1.pm | 5 +++-- examples/pdtmc/nand/nand_20-2.pm | 4 +++- examples/pdtmc/nand/nand_20-3.pm | 5 +++-- examples/pdtmc/nand/nand_20-4.pm | 4 +++- examples/pdtmc/nand/nand_20-5.pm | 4 +++- src/storage/parameters.h | 4 ++-- 11 files changed, 30 insertions(+), 21 deletions(-) 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;