From 799cbce775b7b704fe1bf22b2e0a40a4f76161dd Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 20 Mar 2015 12:36:32 +0100 Subject: [PATCH] Added function tests for CTMC creation and time-bounded reachability. Former-commit-id: e56f860a70dfb524356de59afe0bb9ced3e343da --- examples/ctmc/fms/fms.sm | 126 +++++++++++++ examples/ctmc/tandem/tandem.sm | 38 ++++ .../csl/SparseCtmcCslModelChecker.cpp | 5 + .../builder/ExplicitPrismModelBuilderTest.cpp | 28 +++ test/functional/builder/cluster2.sm | 116 ++++++++++++ test/functional/builder/embedded2.sm | 151 ++++++++++++++++ test/functional/builder/fms2.sm | 126 +++++++++++++ test/functional/builder/polling2.sm | 53 ++++++ test/functional/builder/tandem5.sm | 42 +++++ .../SparseCtmcCslModelCheckerTest.cpp | 169 ++++++++++++++++++ 10 files changed, 854 insertions(+) create mode 100644 examples/ctmc/fms/fms.sm create mode 100644 examples/ctmc/tandem/tandem.sm create mode 100644 test/functional/builder/cluster2.sm create mode 100644 test/functional/builder/embedded2.sm create mode 100644 test/functional/builder/fms2.sm create mode 100644 test/functional/builder/polling2.sm create mode 100644 test/functional/builder/tandem5.sm create mode 100644 test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp diff --git a/examples/ctmc/fms/fms.sm b/examples/ctmc/fms/fms.sm new file mode 100644 index 000000000..318a4a3a8 --- /dev/null +++ b/examples/ctmc/fms/fms.sm @@ -0,0 +1,126 @@ +// flexible manufacturing system [CT93] +// gxn/dxp 11/06/01 + +ctmc // model is a ctmc + +const int n; // number of tokens + +// rates from Pi equal #(Pi) * min(1, np/r) +// where np = (3n)/2 and r = P1+P2+P3+P12 +const int np=floor((3*n)/2); +formula r = P1+P2+P3+P12; + +module machine1 + + P1 : [0..n] init n; + P1wM1 : [0..n]; + P1M1 : [0..3]; + P1d : [0..n]; + P1s : [0..n]; + P1wP2 : [0..n]; + M1 : [0..3] init 3; + + [t1] (P1>0) & (M1>0) & (P1M1<3) -> P1*min(1,np/r) : (P1'=P1-1) & (P1M1'=P1M1+1) & (M1'=M1-1); + [t1] (P1>0) & (M1=0) & (P1wM1 P1*min(1,np/r) : (P1'=P1-1) & (P1wM1'=P1wM1+1); + + [] (P1M1>0) & (P1wM1=0) & (M1<3) & (P1s 0.2*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1s'=P1s+1); + [] (P1M1>0) & (P1wM1>0) & (P1s 0.2*P1M1 : (P1wM1'=P1wM1-1) & (P1s'=P1s+1); + + [] (P1M1>0) & (P2wP1=0) & (P1wM1=0) & (M1<3) & (P1wP2 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1wP2'=P1wP2+1); + [] (P1M1>0) & (P2wP1=0) & (P1wM1>0) & (P1wP2 0.05*P1M1 : (P1wM1'=P1wM1-1) & (P1wP2'=P1wP2+1); + + [p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1=0) & (M1<3) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1); + [p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1>0) -> 0.05*P1M1 : (P1wM1'=P1wM1-1); + + [p1p2] (P1wP2>0) -> 1: (P1wP2'=P1wP2-1); + [] (P1s>0) & (P1+P1s<=n) -> 1/60 : (P1s'=0) & (P1'=P1+P1s); + [fp12] (P1+P12s<=n) -> 1: (P1'=P1+P12s); + +endmodule + +module machine2 + + P2 : [0..n] init n; + P2wM2 : [0..n]; + P2M2 : [0..1]; + P2s : [0..n]; + P2wP1 : [0..n]; + M2 : [0..1] init 1; + + [t2] (P2>0) & (M2>0) & (P2M2<1) -> P2*min(1,np/r) : (P2'=P2-1) & (P2M2'=P2M2+1) & (M2'=M2-1); + [t2] (P2>0) & (M2=0) & (P2wM2 P2*min(1,np/r) : (P2'=P2-1) & (P2wM2'=P2wM2+1); + + [] (P2M2>0) & (P2wM2=0) & (M2<1) & (P2s 0.1 : (P2M2'=P2M2-1) & (M2'=M2+1) & (P2s'=P2s+1); + [] (P2M2>0) & (P2wM2>0) & (P2s 0.1 : (P2wM2'=P2wM2-1) & (P2s'=P2s+1); + + [] (P2M2>0) & (P1wP2=0) & (P2wM2=0) & (M2<1) & (P2wP1 1/15: (P2M2'=P2M2-1) & (M2'=M2+1) & (P2wP1'=P2wP1+1); + [] (P2M2>0) & (P1wP2=0) & (P2wM2>0) & (P2wP1 1/15: (P2wM2'=P2wM2-1) & (P2wP1'=P2wP1+1); + + [p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2=0) & (M2<1) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1); + [p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2>0) -> 1/15: (P2wM2'=P2wM2-1); + + [p1p2] (P2wP1>0) -> 1 : (P2wP1'=P2wP1-1); + [] (P2s>0) & (P2+P2s<=n) -> 1/60 : (P2s'=0) & (P2'=P2+P2s); + [fp12] (P2+P12s<=n) -> 1 : (P2'=P2+P12s); + [p2p3] (M2>0) -> 1 : (M2'=M2); + +endmodule + +module machine3 + + P3 : [0..n] init n; + P3M2 : [0..n]; + P3s : [0..n]; + + [t3] (P3>0) & (P3M2 P3*min(1,np/r) : (P3'=P3-1) & (P3M2'=P3M2+1); + + [p2p3] (P3M2>0) & (P3s 1/2 : (P3M2'=P3M2-1) & (P3s'=P3s+1); + [] (P3s>0) & (P3+P3s<=n) -> 1/60 : (P3s'=0) & (P3'=P3+P3s); + +endmodule + +module machine12 + + P12 : [0..n]; + P12wM3 : [0..n]; + P12M3 : [0..2]; + P12s : [0..n]; + M3 : [0..2] init 2; + + [p1p2] (P12 1: (P12'=P12+1); + + [t12] (P12>0) & (M3>0) & (P12M3<2) -> P12*min(1,np/r) : (P12'=P12-1) & (P12M3'=P12M3+1) & (M3'=M3-1); + [t12] (P12>0) & (M3=0) & (P12wM3 P12*min(1,np/r) : (P12'=P12-1) & (P12wM3'=P12wM3+1); + + [] (P12M3>0) & (P12wM3=0) & (P12s P12M3 : (P12M3'=P12M3-1) & (P12s'=P12s+1) & (M3'=M3+1); + [] (P12M3>0) & (P12wM3>0) & (P12s P12M3 : (P12wM3'=P12wM3-1) & (P12s'=P12s+1); + + [fp12] (P12s>0) -> 1/60 : (P12s'=0); + +endmodule + +// reward structures + +// throughput of machine1 +rewards "throughput_m1" + [t1] true : 1; +endrewards +// throughput of machine2 +rewards "throughput_m2" + [t2] true : 1; +endrewards +// throughput of machine3 +rewards "throughput_m3" + [t3] true : 1; +endrewards +// throughput of machine12 +rewards "throughput_m12" + [t12] true : 1; +endrewards +// productivity of the system +rewards "productivity" + [t1] true : 400; + [t2] true : 600; + [t3] true : 100; + [t12] true : 1100; +endrewards diff --git a/examples/ctmc/tandem/tandem.sm b/examples/ctmc/tandem/tandem.sm new file mode 100644 index 000000000..439d33813 --- /dev/null +++ b/examples/ctmc/tandem/tandem.sm @@ -0,0 +1,38 @@ +// tandem queueing network [HKMKS99] +// gxn/dxp 25/01/00 + +ctmc + +const int c; // queue capacity + +const double lambda = 4*c; +const double mu1a = 0.1*2; +const double mu1b = 0.9*2; +const double mu2 = 2; +const double kappa = 4; + +module serverC + + sc : [0..c]; + ph : [1..2]; + + [] (sc lambda: (sc'=sc+1); + [route] (sc>0) & (ph=1) -> mu1b: (sc'=sc-1); + [] (sc>0) & (ph=1) -> mu1a: (ph'=2); + [route] (sc>0) & (ph=2) -> mu2: (ph'=1) & (sc'=sc-1); + +endmodule + +module serverM + + sm : [0..c]; + + [route] (sm 1: (sm'=sm+1); + [] (sm>0) -> kappa: (sm'=sm-1); + +endmodule + +// reward - number of customers in network +rewards "customers" + true : sc + sm; +endrewards \ No newline at end of file diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 6e432c754..828542bef 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -228,6 +228,11 @@ namespace storm { template std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, ValueType const& lambda, std::vector values, storm::solver::LinearEquationSolver const& linearEquationSolver) const { + // If no time can pass, the current values are the result. + if (lambda == storm::utility::zero()) { + return values; + } + // Use Fox-Glynn to get the truncation points and the weights. std::tuple> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::generalSettings().getPrecision() / 8.0); diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index 0ff231130..7e7599246 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -32,6 +32,34 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) { EXPECT_EQ(2505, model->getNumberOfTransitions()); } +TEST(ExplicitPrismModelBuilderTest, Ctmc) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(276, model->getNumberOfStates()); + EXPECT_EQ(1120, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(3478, model->getNumberOfStates()); + EXPECT_EQ(14639, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(12, model->getNumberOfStates()); + EXPECT_EQ(22, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(810, model->getNumberOfStates()); + EXPECT_EQ(3699, model->getNumberOfTransitions()); + + program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + EXPECT_EQ(66, model->getNumberOfStates()); + EXPECT_EQ(189, model->getNumberOfTransitions()); +} + TEST(ExplicitPrismModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); diff --git a/test/functional/builder/cluster2.sm b/test/functional/builder/cluster2.sm new file mode 100644 index 000000000..5afd88f47 --- /dev/null +++ b/test/functional/builder/cluster2.sm @@ -0,0 +1,116 @@ +// Workstation cluster [HHK00] +// dxp/gxn 11/01/00 + +ctmc + +const int N = 2; // Number of workstations in each cluster +const int left_mx = N; // Number of work stations in left cluster +const int right_mx = N; // Number of work stations in right cluster + +// Failure rates +const double ws_fail = 1/500; // Single workstation: average time to fail = 500 hrs +const double switch_fail = 1/4000; // Switch: average time to fail = 4000 hrs +const double line_fail = 1/5000; // Backbone: average time to fail = 5000 hrs + +// Left cluster +module Left + + left_n : [0..left_mx] init left_mx; // Number of workstations operational + left : bool; // Being repaired? + + [startLeft] !left & (left_n 1 : (left'=true); + [repairLeft] left & (left_n 1 : (left'=false) & (left_n'=left_n+1); + [] (left_n>0) -> ws_fail*left_n : (left_n'=left_n-1); + +endmodule + +// Right cluster +module Right = Left[left_n=right_n, + left=right, + left_mx=right_mx, + startLeft=startRight, + repairLeft=repairRight ] +endmodule + +// Repair unit +module Repairman + + r : bool; // Repairing? + + [startLeft] !r -> 10 : (r'=true); // Inspect Left + [startRight] !r -> 10 : (r'=true); // Inspect Right + [startToLeft] !r -> 10 : (r'=true); // Inspect ToLeft + [startToRight] !r -> 10 : (r'=true); // Inspect ToRight + [startLine] !r -> 10 : (r'=true); // Inspect Line + + [repairLeft] r -> 2 : (r'=false); // Repair Left + [repairRight] r -> 2 : (r'=false); // Repair Right + [repairToLeft] r -> 0.25 : (r'=false); // Repair ToLeft + [repairToRight] r -> 0.25 : (r'=false); // Repair ToRight + [repairLine] r -> 0.125 : (r'=false); // Repair Line + +endmodule + +// Line/backbone +module Line + + line : bool; // Being repaired? + line_n : bool init true; // Working? + + [startLine] !line & !line_n -> 1 : (line'=true); + [repairLine] line & !line_n -> 1 : (line'=false) & (line_n'=true); + [] line_n -> line_fail : (line_n'=false); + +endmodule + +// Left switch +module ToLeft = Line[line=toleft, + line_n=toleft_n, + line_fail=switch_fail, + startLine=startToLeft, + repairLine=repairToLeft ] +endmodule + +// Right switch +module ToRight = Line[line=toright, + line_n=toright_n, + line_fail=switch_fail, + startLine=startToRight, + repairLine=repairToRight ] +endmodule + +// Formulas + labels + +// Minimum QoS requires 3/4 connected workstations operational +const int k = floor(0.75*N); +// left_operational_i : left_n>=i & toleft_n +// right_operational_i : right_n>=i & toright_n +// operational_i : (left_n+right_n)>=i & toleft_n & line_n & toright_n +// minimum_k : left_operational_k | right_operational_k | operational_k +formula minimum = (left_n>=k & toleft_n) | + (right_n>=k & toright_n) | + ((left_n+right_n)>=k & toleft_n & line_n & toright_n); +label "minimum" = (left_n>=k & toleft_n) | (right_n>=k & toright_n) | ((left_n+right_n)>=k & toleft_n & line_n & toright_n); +// premium = minimum_N +label "premium" = (left_n>=left_mx & toleft_n) | (right_n>=right_mx & toright_n) | ((left_n+right_n)>=left_mx & toleft_n & line_n & toright_n); + +// Reward structures + +// Percentage of operational workstations stations +rewards "percent_op" + true : 100*(left_n+right_n)/(2*N); +endrewards + +// Time that the system is not delivering at least minimum QoS +rewards "time_not_min" + !minimum : 1; +endrewards + +// Number of repairs +rewards "num_repairs" + [repairLeft] true : 1; + [repairRight] true : 1; + [repairToLeft] true : 1; + [repairToRight] true : 1; + [repairLine] true : 1; +endrewards diff --git a/test/functional/builder/embedded2.sm b/test/functional/builder/embedded2.sm new file mode 100644 index 000000000..6d64d949e --- /dev/null +++ b/test/functional/builder/embedded2.sm @@ -0,0 +1,151 @@ +ctmc + +// constants +const int MAX_COUNT = 2; +const int MIN_SENSORS = 2; +const int MIN_ACTUATORS = 1; + +// rates +const double lambda_p = 1/(365*24*60*60); // 1 year +const double lambda_s = 1/(30*24*60*60); // 1 month +const double lambda_a = 1/(2*30*24*60*60); // 2 months +const double tau = 1/60; // 1 min +const double delta_f = 1/(24*60*60); // 1 day +const double delta_r = 1/30; // 30 secs + +// sensors +module sensors + + s : [0..3] init 3; // number of sensors working + + [] s>1 -> s*lambda_s : (s'=s-1); // failure of a single sensor + +endmodule + +// input processor +// (takes data from sensors and passes onto main processor) +module proci + + i : [0..2] init 2; // 2=ok, 1=transient fault, 0=failed + + [] i>0 & s>=MIN_SENSORS -> lambda_p : (i'=0); // failure of processor + [] i=2 & s>=MIN_SENSORS -> delta_f : (i'=1); // transient fault + [input_reboot] i=1 & s>=MIN_SENSORS -> delta_r : (i'=2); // reboot after transient fault + +endmodule + +// actuators +module actuators + + a : [0..2] init 2; // number of actuators working + + [] a>0 -> a*lambda_a : (a'=a-1); // failure of a single actuator + +endmodule + +// output processor +// (receives instructions from main processor and passes onto actuators) +module proco = proci [ i=o, s=a, input_reboot=output_reboot, MIN_SENSORS=MIN_ACTUATORS ] endmodule + +// main processor +// (takes data from proci, processes it, and passes instructions to proco) +module procm + + m : [0..1] init 1; // 1=ok, 0=failed + count : [0..MAX_COUNT+1] init 0; // number of consecutive skipped cycles + + // failure of processor + [] m=1 -> lambda_p : (m'=0); + // processing completed before timer expires - reset skipped cycle counter + [timeout] comp -> tau : (count'=0); + // processing not completed before timer expires - increment skipped cycle counter + [timeout] !comp -> tau : (count'=min(count+1, MAX_COUNT+1)); + +endmodule + +// connecting bus +module bus + + // flags + // main processor has processed data from input processor + // and sent corresponding instructions to output processor (since last timeout) + comp : bool init true; + // input processor has data ready to send + reqi : bool init true; + // output processor has instructions ready to be processed + reqo : bool init false; + + // input processor reboots + [input_reboot] true -> 1 : + // performs a computation if has already done so or + // it is up and ouput clear (i.e. nothing waiting) + (comp'=(comp | (m=1 & !reqo))) + // up therefore something to process + & (reqi'=true) + // something to process if not functioning and either + // there is something already pending + // or the main processor sends a request + & (reqo'=!(o=2 & a>=1) & (reqo | m=1)); + + // output processor reboots + [output_reboot] true -> 1 : + // performs a computation if it has already or + // something waiting and is up + // (can be processes as the output has come up and cleared pending requests) + (comp'=(comp | (reqi & m=1))) + // something to process it they are up or + // there was already something and the main processor acts + // (output now up must be due to main processor being down) + & (reqi'=(i=2 & s>=2) | (reqi & m=0)) + // output and actuators up therefore nothing can be pending + & (reqo'=false); + + // main processor times out + [timeout] true -> 1 : + // performs a computation if it is up something was pending + // and nothing is waiting for the output + (comp'=(reqi & !reqo & m=1)) + // something to process if up or + // already something and main process cannot act + // (down or outputs pending) + & (reqi'=(i=2 & s>=2) | (reqi & (reqo | m=0))) + // something to process if they are not functioning and + // either something is already pending + // or the main processor acts + & (reqo'=!(o=2 & a>=1) & (reqo | (reqi & m=1))); + +endmodule + + +// the system is down +formula down = (i=2&s0) & (M1>0) & (P1M1<3) -> P1*min(1,np/r) : (P1'=P1-1) & (P1M1'=P1M1+1) & (M1'=M1-1); + [t1] (P1>0) & (M1=0) & (P1wM1 P1*min(1,np/r) : (P1'=P1-1) & (P1wM1'=P1wM1+1); + + [] (P1M1>0) & (P1wM1=0) & (M1<3) & (P1s 0.2*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1s'=P1s+1); + [] (P1M1>0) & (P1wM1>0) & (P1s 0.2*P1M1 : (P1wM1'=P1wM1-1) & (P1s'=P1s+1); + + [] (P1M1>0) & (P2wP1=0) & (P1wM1=0) & (M1<3) & (P1wP2 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1wP2'=P1wP2+1); + [] (P1M1>0) & (P2wP1=0) & (P1wM1>0) & (P1wP2 0.05*P1M1 : (P1wM1'=P1wM1-1) & (P1wP2'=P1wP2+1); + + [p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1=0) & (M1<3) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1); + [p1p2] (P1M1>0) & (P2wP1>0) & (P1wM1>0) -> 0.05*P1M1 : (P1wM1'=P1wM1-1); + + [p1p2] (P1wP2>0) -> 1: (P1wP2'=P1wP2-1); + [] (P1s>0) & (P1+P1s<=n) -> 1/60 : (P1s'=0) & (P1'=P1+P1s); + [fp12] (P1+P12s<=n) -> 1: (P1'=P1+P12s); + +endmodule + +module machine2 + + P2 : [0..n] init n; + P2wM2 : [0..n]; + P2M2 : [0..1]; + P2s : [0..n]; + P2wP1 : [0..n]; + M2 : [0..1] init 1; + + [t2] (P2>0) & (M2>0) & (P2M2<1) -> P2*min(1,np/r) : (P2'=P2-1) & (P2M2'=P2M2+1) & (M2'=M2-1); + [t2] (P2>0) & (M2=0) & (P2wM2 P2*min(1,np/r) : (P2'=P2-1) & (P2wM2'=P2wM2+1); + + [] (P2M2>0) & (P2wM2=0) & (M2<1) & (P2s 0.1 : (P2M2'=P2M2-1) & (M2'=M2+1) & (P2s'=P2s+1); + [] (P2M2>0) & (P2wM2>0) & (P2s 0.1 : (P2wM2'=P2wM2-1) & (P2s'=P2s+1); + + [] (P2M2>0) & (P1wP2=0) & (P2wM2=0) & (M2<1) & (P2wP1 1/15: (P2M2'=P2M2-1) & (M2'=M2+1) & (P2wP1'=P2wP1+1); + [] (P2M2>0) & (P1wP2=0) & (P2wM2>0) & (P2wP1 1/15: (P2wM2'=P2wM2-1) & (P2wP1'=P2wP1+1); + + [p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2=0) & (M2<1) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1); + [p1p2] (P2M2>0) & (P1wP2>0) & (P2wM2>0) -> 1/15: (P2wM2'=P2wM2-1); + + [p1p2] (P2wP1>0) -> 1 : (P2wP1'=P2wP1-1); + [] (P2s>0) & (P2+P2s<=n) -> 1/60 : (P2s'=0) & (P2'=P2+P2s); + [fp12] (P2+P12s<=n) -> 1 : (P2'=P2+P12s); + [p2p3] (M2>0) -> 1 : (M2'=M2); + +endmodule + +module machine3 + + P3 : [0..n] init n; + P3M2 : [0..n]; + P3s : [0..n]; + + [t3] (P3>0) & (P3M2 P3*min(1,np/r) : (P3'=P3-1) & (P3M2'=P3M2+1); + + [p2p3] (P3M2>0) & (P3s 1/2 : (P3M2'=P3M2-1) & (P3s'=P3s+1); + [] (P3s>0) & (P3+P3s<=n) -> 1/60 : (P3s'=0) & (P3'=P3+P3s); + +endmodule + +module machine12 + + P12 : [0..n]; + P12wM3 : [0..n]; + P12M3 : [0..2]; + P12s : [0..n]; + M3 : [0..2] init 2; + + [p1p2] (P12 1: (P12'=P12+1); + + [t12] (P12>0) & (M3>0) & (P12M3<2) -> P12*min(1,np/r) : (P12'=P12-1) & (P12M3'=P12M3+1) & (M3'=M3-1); + [t12] (P12>0) & (M3=0) & (P12wM3 P12*min(1,np/r) : (P12'=P12-1) & (P12wM3'=P12wM3+1); + + [] (P12M3>0) & (P12wM3=0) & (P12s P12M3 : (P12M3'=P12M3-1) & (P12s'=P12s+1) & (M3'=M3+1); + [] (P12M3>0) & (P12wM3>0) & (P12s P12M3 : (P12wM3'=P12wM3-1) & (P12s'=P12s+1); + + [fp12] (P12s>0) -> 1/60 : (P12s'=0); + +endmodule + +// reward structures + +// throughput of machine1 +rewards "throughput_m1" + [t1] true : 1; +endrewards +// throughput of machine2 +rewards "throughput_m2" + [t2] true : 1; +endrewards +// throughput of machine3 +rewards "throughput_m3" + [t3] true : 1; +endrewards +// throughput of machine12 +rewards "throughput_m12" + [t12] true : 1; +endrewards +// productivity of the system +rewards "productivity" + [t1] true : 400; + [t2] true : 600; + [t3] true : 100; + [t12] true : 1100; +endrewards diff --git a/test/functional/builder/polling2.sm b/test/functional/builder/polling2.sm new file mode 100644 index 000000000..8fdc2f7fd --- /dev/null +++ b/test/functional/builder/polling2.sm @@ -0,0 +1,53 @@ +// polling example [IT90] +// gxn/dxp 26/01/00 + +ctmc + +const int N = 2; + +const double mu = 1; +const double gamma = 200; +const double lambda = mu/N; + +module server + + s : [1..2]; // station + a : [0..1]; // action: 0=polling, 1=serving + + [loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); + [loop1b] (s=1)&(a=0) -> gamma : (a'=1); + [serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop2a] (s=2)&(a=0) -> gamma : (s'=1); + [loop2b] (s=2)&(a=0) -> gamma : (a'=1); + [serve2] (s=2)&(a=1) -> mu : (s'=1)&(a'=0); + +endmodule + +module station1 + + s1 : [0..1]; // state of station: 0=empty, 1=full + + [loop1a] (s1=0) -> 1 : (s1'=0); + [] (s1=0) -> lambda : (s1'=1); + [loop1b] (s1=1) -> 1 : (s1'=1); + [serve1] (s1=1) -> 1 : (s1'=0); + +endmodule + +// construct further stations through renaming + +module station2 = station1 [ s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2 ] endmodule +// (cumulative) rewards + +// expected time station 1 is waiting to be served +rewards "waiting" + s1=1 & !(s=1 & a=1) : 1; +endrewards + +// expected number of times station 1 is served +rewards "served" + [serve1] true : 1; +endrewards + +label "target" = s=1&a=0; diff --git a/test/functional/builder/tandem5.sm b/test/functional/builder/tandem5.sm new file mode 100644 index 000000000..36c5f08af --- /dev/null +++ b/test/functional/builder/tandem5.sm @@ -0,0 +1,42 @@ +// tandem queueing network [HKMKS99] +// gxn/dxp 25/01/00 + +ctmc + +const int c = 5; // queue capacity + +const double lambda = 4*c; +const double mu1a = 0.1*2; +const double mu1b = 0.9*2; +const double mu2 = 2; +const double kappa = 4; + +module serverC + + sc : [0..c]; + ph : [1..2]; + + [] (sc lambda: (sc'=sc+1); + [route] (sc>0) & (ph=1) -> mu1b: (sc'=sc-1); + [] (sc>0) & (ph=1) -> mu1a: (ph'=2); + [route] (sc>0) & (ph=2) -> mu2: (ph'=1) & (sc'=sc-1); + +endmodule + +module serverM + + sm : [0..c]; + + [route] (sm 1: (sm'=sm+1); + [] (sm>0) -> kappa: (sm'=sm-1); + +endmodule + +// reward - number of customers in network +rewards "customers" + true : sc + sm; +endrewards + +label "network_full" = sc=c&sm=c&ph=2; +label "first_queue_full" = sc=c; +label "second_queue_full" = sm=c; diff --git a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp new file mode 100644 index 000000000..86792fe8d --- /dev/null +++ b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp @@ -0,0 +1,169 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "src/parser/PrismParser.h" +#include "src/parser/FormulaParser.h" +#include "src/logic/Formulas.h" +#include "src/builder/ExplicitPrismModelBuilder.h" + +#include "src/solver/NativeLinearEquationSolver.h" +#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/settings/SettingsManager.h" + +TEST(SparseCtmcCslModelCheckerTest, Cluster) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + + // Start checking properties. + formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); +} + +TEST(SparseCtmcCslModelCheckerTest, Embedded) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + + // Start checking properties. + formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); +} + +TEST(SparseCtmcCslModelCheckerTest, Polling) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + + // Start checking properties. + formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); +} + +TEST(SparseCtmcCslModelCheckerTest, Fms) { + // No properties to check at this point. +} + +TEST(SparseCtmcCslModelCheckerTest, Tandem) { + // Parse the model description. + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); + storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); + std::shared_ptr formula(nullptr); + + // Build the model. + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::translateProgram(program); + ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); + std::shared_ptr> ctmc = model->as>(); + uint_fast64_t initialState = *ctmc->getInitialStates().begin(); + + // Create model checker. + storm::modelchecker::SparseCtmcCslModelChecker modelchecker(*ctmc); + + // Start checking properties. + formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); + std::unique_ptr checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision()); + + formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]"); + checkResult = modelchecker.check(*formula); + + ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); + storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); + EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); +}