sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added function tests for CTMC creation and time-bounded reachability. 

Former-commit-id: e56f860a70
main
dehnert 11 years ago
parent
ccc60ef145
commit
799cbce775
10 changed files with 854 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 126
      examples/ctmc/fms/fms.sm
  2. 38
      examples/ctmc/tandem/tandem.sm
  3. 5
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  4. 28
      test/functional/builder/ExplicitPrismModelBuilderTest.cpp
  5. 116
      test/functional/builder/cluster2.sm
  6. 151
      test/functional/builder/embedded2.sm
  7. 126
      test/functional/builder/fms2.sm
  8. 53
      test/functional/builder/polling2.sm
  9. 42
      test/functional/builder/tandem5.sm
  10. 169
      test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp

126
examples/ctmc/fms/fms.sm
View File

@ -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<n) -> P1*min(1,np/r) : (P1'=P1-1) & (P1wM1'=P1wM1+1);
[] (P1M1>0) & (P1wM1=0) & (M1<3) & (P1s<n) -> 0.2*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1s'=P1s+1);
[] (P1M1>0) & (P1wM1>0) & (P1s<n) -> 0.2*P1M1 : (P1wM1'=P1wM1-1) & (P1s'=P1s+1);
[] (P1M1>0) & (P2wP1=0) & (P1wM1=0) & (M1<3) & (P1wP2<n) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1wP2'=P1wP2+1);
[] (P1M1>0) & (P2wP1=0) & (P1wM1>0) & (P1wP2<n) -> 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<n) -> P2*min(1,np/r) : (P2'=P2-1) & (P2wM2'=P2wM2+1);
[] (P2M2>0) & (P2wM2=0) & (M2<1) & (P2s<n) -> 0.1 : (P2M2'=P2M2-1) & (M2'=M2+1) & (P2s'=P2s+1);
[] (P2M2>0) & (P2wM2>0) & (P2s<n) -> 0.1 : (P2wM2'=P2wM2-1) & (P2s'=P2s+1);
[] (P2M2>0) & (P1wP2=0) & (P2wM2=0) & (M2<1) & (P2wP1<n) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1) & (P2wP1'=P2wP1+1);
[] (P2M2>0) & (P1wP2=0) & (P2wM2>0) & (P2wP1<n) -> 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<n) -> P3*min(1,np/r) : (P3'=P3-1) & (P3M2'=P3M2+1);
[p2p3] (P3M2>0) & (P3s<n) -> 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<n) -> 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<n) -> P12*min(1,np/r) : (P12'=P12-1) & (P12wM3'=P12wM3+1);
[] (P12M3>0) & (P12wM3=0) & (P12s<n) & (M3<2) -> P12M3 : (P12M3'=P12M3-1) & (P12s'=P12s+1) & (M3'=M3+1);
[] (P12M3>0) & (P12wM3>0) & (P12s<n) -> 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

38
examples/ctmc/tandem/tandem.sm
View File

@ -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<c) -> 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<c) -> 1: (sm'=sm+1);
[] (sm>0) -> kappa: (sm'=sm-1);
endmodule
// reward - number of customers in network
rewards "customers"
true : sc + sm;
endrewards

5
src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -228,6 +228,11 @@ namespace storm {
template<class ValueType> template<class ValueType>
std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType const& lambda, std::vector<ValueType> values, storm::solver::LinearEquationSolver<ValueType> const& linearEquationSolver) const { std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType const& lambda, std::vector<ValueType> values, storm::solver::LinearEquationSolver<ValueType> const& linearEquationSolver) const {
// If no time can pass, the current values are the result.
if (lambda == storm::utility::zero<ValueType>()) {
return values;
}
// Use Fox-Glynn to get the truncation points and the weights. // Use Fox-Glynn to get the truncation points and the weights.
std::tuple<uint_fast64_t, uint_fast64_t, ValueType, std::vector<ValueType>> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::generalSettings().getPrecision() / 8.0); std::tuple<uint_fast64_t, uint_fast64_t, ValueType, std::vector<ValueType>> foxGlynnResult = storm::utility::numerical::getFoxGlynnCutoff(lambda, 1e-300, 1e+300, storm::settings::generalSettings().getPrecision() / 8.0);

28
test/functional/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -32,6 +32,34 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) {
EXPECT_EQ(2505, model->getNumberOfTransitions()); 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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::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<double>::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<double>::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<double>::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<double>::translateProgram(program);
EXPECT_EQ(66, model->getNumberOfStates());
EXPECT_EQ(189, model->getNumberOfTransitions());
}
TEST(ExplicitPrismModelBuilderTest, Mdp) { TEST(ExplicitPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");

116
test/functional/builder/cluster2.sm
View File

@ -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<left_mx) -> 1 : (left'=true);
[repairLeft] left & (left_n<left_mx) -> 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

151
test/functional/builder/embedded2.sm
View File

@ -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&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0);
// transient failure has occured but the system is not down
formula danger = !down & (i=1 | o=1);
// the system is operational
formula up = !down & !danger;
// reward structures
rewards "up"
up : 1/3600;
endrewards
rewards "danger"
danger : 1/3600;
endrewards
rewards "down"
down : 1/3600;
endrewards
//labels
// causes of failues
label "fail_sensors" = i=2&s<MIN_SENSORS; // sensors have failed
label "fail_actuators" = o=2&a<MIN_ACTUATORS; // actuators have failed
label "fail_io" = count=MAX_COUNT+1; // IO has failed
label "fail_main" = m=0; // ,main processor has failed
// system status
label "down" = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0); // system has shutdown
label "danger" = !down & (i=1 | o=1); // transient fault has occured
label "up" = !down & !danger;

126
test/functional/builder/fms2.sm
View File

@ -0,0 +1,126 @@
// flexible manufacturing system [CT93]
// gxn/dxp 11/06/01
ctmc // model is a ctmc
const int n = 2; // 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<n) -> P1*min(1,np/r) : (P1'=P1-1) & (P1wM1'=P1wM1+1);
[] (P1M1>0) & (P1wM1=0) & (M1<3) & (P1s<n) -> 0.2*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1s'=P1s+1);
[] (P1M1>0) & (P1wM1>0) & (P1s<n) -> 0.2*P1M1 : (P1wM1'=P1wM1-1) & (P1s'=P1s+1);
[] (P1M1>0) & (P2wP1=0) & (P1wM1=0) & (M1<3) & (P1wP2<n) -> 0.05*P1M1 : (P1M1'=P1M1-1) & (M1'=M1+1) & (P1wP2'=P1wP2+1);
[] (P1M1>0) & (P2wP1=0) & (P1wM1>0) & (P1wP2<n) -> 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<n) -> P2*min(1,np/r) : (P2'=P2-1) & (P2wM2'=P2wM2+1);
[] (P2M2>0) & (P2wM2=0) & (M2<1) & (P2s<n) -> 0.1 : (P2M2'=P2M2-1) & (M2'=M2+1) & (P2s'=P2s+1);
[] (P2M2>0) & (P2wM2>0) & (P2s<n) -> 0.1 : (P2wM2'=P2wM2-1) & (P2s'=P2s+1);
[] (P2M2>0) & (P1wP2=0) & (P2wM2=0) & (M2<1) & (P2wP1<n) -> 1/15: (P2M2'=P2M2-1) & (M2'=M2+1) & (P2wP1'=P2wP1+1);
[] (P2M2>0) & (P1wP2=0) & (P2wM2>0) & (P2wP1<n) -> 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<n) -> P3*min(1,np/r) : (P3'=P3-1) & (P3M2'=P3M2+1);
[p2p3] (P3M2>0) & (P3s<n) -> 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<n) -> 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<n) -> P12*min(1,np/r) : (P12'=P12-1) & (P12wM3'=P12wM3+1);
[] (P12M3>0) & (P12wM3=0) & (P12s<n) & (M3<2) -> P12M3 : (P12M3'=P12M3-1) & (P12s'=P12s+1) & (M3'=M3+1);
[] (P12M3>0) & (P12wM3>0) & (P12s<n) -> 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

53
test/functional/builder/polling2.sm
View File

@ -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;

42
test/functional/builder/tandem5.sm
View File

@ -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<c) -> 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<c) -> 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;

169
test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp
View File

@ -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<storm::logic::Formula> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc);
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<storm::logic::Formula> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc);
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<storm::logic::Formula> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc);
// Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<storm::logic::Formula> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc);
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
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<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
}
Write Preview
Loading…
Cancel
Save