From e4968b1ddee0819fd399366e321398f39dcc66ea Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 24 Apr 2015 08:59:34 +0200
Subject: [PATCH] Fixed minor issue in cli
Former-commit-id: ed63925765551ec91d8db0262e6797c4de6d3fe8
---
examples/dtmc/crowds/crowds15_5.pm | 6 +++---
examples/dtmc/crowds/crowds20_5.pm | 7 ++++---
src/utility/cli.h | 2 +-
3 files changed, 8 insertions(+), 7 deletions(-)
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<ValueType> modelchecker2(*dtmc);
if (modelchecker2.canHandle(*formula.get())) {
- modelchecker2.check(*formula.get());
+ result = modelchecker2.check(*formula.get());
}
}
} else if (model->getType() == storm::models::ModelType::Mdp) {