diff --git a/examples/dtmc/crowds/crowds15_5.pm b/examples/dtmc/crowds/crowds15_5.pm index 511d962f0..95ab8a910 100644 --- a/examples/dtmc/crowds/crowds15_5.pm +++ b/examples/dtmc/crowds/crowds15_5.pm @@ -2,9 +2,9 @@ dtmc // probability of forwarding const double PF = 0.8; -const double notPF = .2; // must be 1-PF +const double notPF = 0.2; // must be 1-PF // probability that a crowd member is bad -const double badC = .167; +const double badC = 0.167; // probability that a crowd member is good const double goodC = 0.833; // Total number of protocol runs to analyze @@ -92,4 +92,4 @@ endmodule label "observe0Greater1" = observe0 > 1; label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1; -label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1; \ No newline at end of file +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1; diff --git a/examples/dtmc/crowds/crowds20_5.pm b/examples/dtmc/crowds/crowds20_5.pm index 31c63770a..1809c22d7 100644 --- a/examples/dtmc/crowds/crowds20_5.pm +++ b/examples/dtmc/crowds/crowds20_5.pm @@ -2,9 +2,9 @@ dtmc // probability of forwarding const double PF = 0.8; -const double notPF = .2; // must be 1-PF +const double notPF = 0.2; // must be 1-PF // probability that a crowd member is bad -const double badC = .167; +const double badC = 0.167; // probability that a crowd member is good const double goodC = 0.833; // Total number of protocol runs to analyze @@ -107,4 +107,5 @@ endmodule label "observe0Greater1" = observe0 > 1; label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1 | observe5 > 1 | observe6 > 1 | observe7 > 1 | observe8 > 1 | observe9 > 1 | observe10 > 1 | observe11 > 1 | observe12 > 1 | observe13 > 1 | observe14 > 1 | observe15 > 1 | observe16 > 1 | observe17 > 1 | observe18 > 1 | observe19 > 1; -label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1 & observe15 <= 1 & observe16 <= 1 & observe17 <= 1 & observe18 <= 1 & observe19 <= 1; \ No newline at end of file +label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1 & observe5 <= 1 & observe6 <= 1 & observe7 <= 1 & observe8 <= 1 & observe9 <= 1 & observe10 <= 1 & observe11 <= 1 & observe12 <= 1 & observe13 <= 1 & observe14 <= 1 & observe15 <= 1 & observe16 <= 1 & observe17 <= 1 & observe18 <= 1 & observe19 <= 1; + diff --git a/src/utility/cli.h b/src/utility/cli.h index 780201cf3..7fd03536d 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -426,7 +426,7 @@ namespace storm { } else { storm::modelchecker::SparseDtmcEliminationModelChecker modelchecker2(*dtmc); if (modelchecker2.canHandle(*formula.get())) { - modelchecker2.check(*formula.get()); + result = modelchecker2.check(*formula.get()); } } } else if (model->getType() == storm::models::ModelType::Mdp) {