From 0776d8a74b1e3e69b94fd27f2355779671b14369 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 6 Oct 2014 22:19:34 +0200
Subject: [PATCH] Added and fixed some example models. Added option for maximal
size of SCC that gets eliminated using state elimination.
Former-commit-id: bf1e73ff61fc82faa4c434ccb1ff51739ed2ebc6
---
examples/pdtmc/crowds/crowds3_5.pm | 191 ------------------
examples/pdtmc/nand/nand_10-2.pm | 0
examples/pdtmc/nand/nand_10-3.pm | 0
examples/pdtmc/nand/nand_10-4.pm | 0
examples/pdtmc/nand/nand_10-5.pm | 2 +-
.../reachability/SparseSccModelChecker.cpp | 12 +-
.../reachability/SparseSccModelChecker.h | 5 +-
src/settings/modules/ParametricSettings.cpp | 7 +
src/settings/modules/ParametricSettings.h | 8 +
.../expressions/ExpressionEvaluation.h | 1 -
src/utility/cli.h | 1 +
src/utility/macros.h | 12 +-
12 files changed, 29 insertions(+), 210 deletions(-)
delete mode 100644 examples/pdtmc/crowds/crowds3_5.pm
mode change 100755 => 100644 examples/pdtmc/nand/nand_10-2.pm
mode change 100755 => 100644 examples/pdtmc/nand/nand_10-3.pm
mode change 100755 => 100644 examples/pdtmc/nand/nand_10-4.pm
mode change 100755 => 100644 examples/pdtmc/nand/nand_10-5.pm
diff --git a/examples/pdtmc/crowds/crowds3_5.pm b/examples/pdtmc/crowds/crowds3_5.pm
deleted file mode 100644
index 30d84a9d0..000000000
--- a/examples/pdtmc/crowds/crowds3_5.pm
+++ /dev/null
@@ -1,191 +0,0 @@
-// CROWDS [Reiter,Rubin]
-// Vitaly Shmatikov, 2002
-// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de)
-
-// note:
-// Change everything marked CWDSIZ when changing the size of the crowd
-// Change everything marked CWDMAX when increasing max size of the crowd
-
-dtmc
-
-// Model parameters
-const double PF; // forwarding probability
-const double badC; // probability that member is untrustworthy
-
-// Probability of forwarding
-// const double PF = 0.8;
-// const double notPF = 0.2; // must be 1-PF
-
-// Probability that a crowd member is bad
-// const double badC = 0.1;
-// const double badC = 0.091;
-// const double badC = 0.167;
-// const double goodC = 0.909; // must be 1-badC
-// const double goodC = 0.833; // must be 1-badC
-
-const int CrowdSize = 3; // CWDSIZ: actual number of good crowd members
-const int TotalRuns = 5; // Total number of protocol runs to analyze
-const int MaxGood=20; // CWDMAX: maximum number of good crowd members
-
-// Process definitions
-module crowds
-
- // Auxiliary variables
- launch: bool init true; // Start modeling?
- newInstance: bool; // Initialize a new protocol instance?
- runCount: [0..TotalRuns]; // Counts protocol instances
- start: bool; // Start the protocol?
- run: bool; // Run the protocol?
- lastSeen: [0..MaxGood]; // Last crowd member to touch msg
- good: bool; // Crowd member is good?
- bad: bool; // ... bad?
- recordLast: bool; // Record last seen crowd member?
- badObserve: bool; // Bad members observes who sent msg?
- deliver: bool; // Deliver message to destination?
- done: bool; // Protocol instance finished?
-
- // Counters for attackers' observations
- // CWDMAX: 1 counter per each good crowd member
- observe0: [0..TotalRuns];
- observe1: [0..TotalRuns];
- observe2: [0..TotalRuns];
- observe3: [0..TotalRuns];
- observe4: [0..TotalRuns];
- observe5: [0..TotalRuns];
- observe6: [0..TotalRuns];
- observe7: [0..TotalRuns];
- observe8: [0..TotalRuns];
- observe9: [0..TotalRuns];
- observe10: [0..TotalRuns];
- observe11: [0..TotalRuns];
- observe12: [0..TotalRuns];
- observe13: [0..TotalRuns];
- observe14: [0..TotalRuns];
- observe15: [0..TotalRuns];
- observe16: [0..TotalRuns];
- observe17: [0..TotalRuns];
- observe18: [0..TotalRuns];
- observe19: [0..TotalRuns];
-
- [] launch -> (newInstance'=true) & (runCount'=TotalRuns) & (launch'=false);
- // Set up a newInstance protocol instance
- [] newInstance & runCount>0 -> (runCount'=runCount-1) & (newInstance'=false) & (start'=true);
-
- // SENDER
- // Start the protocol
- [] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false);
-
- // CROWD MEMBERS
- // Good or bad crowd member?
- [] !good & !bad & !deliver & run ->
- 1-badC : (good'=true) & (recordLast'=true) & (run'=false) +
- badC : (bad'=true) & (badObserve'=true) & (run'=false);
-
- // GOOD MEMBERS
- // Forward with probability PF, else deliver
- [] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true);
- // Record the last crowd member who touched the msg;
- // all good members may appear with equal probability
- // Note: This is backward. In the real protocol, each honest
- // forwarder randomly chooses the next forwarder.
- // Here, the identity of an honest forwarder is randomly
- // chosen *after* it has forwarded the message.
- [] recordLast & CrowdSize=2 ->
- 1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
- 1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true);
- [] recordLast & CrowdSize=3 ->
- 1/3 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
- 1/3 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
- 1/3 : (lastSeen'=2) & (recordLast'=false) & (run'=true);
- [] recordLast & CrowdSize=4 ->
- 1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
- 1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
- 1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
- 1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true);
- [] recordLast & CrowdSize=5 ->
- 1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
- 1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
- 1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
- 1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
- 1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true);
- [] recordLast & CrowdSize=10 ->
- 1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
- 1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true);
- [] recordLast & CrowdSize=15 ->
- 1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
- 1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true);
- [] recordLast & CrowdSize=20 ->
- 1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) +
- 1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true);
-
- // BAD MEMBERS
- // Remember from whom the message was received and deliver
- // CWDMAX: 1 rule per each good crowd member
- [] lastSeen=0 & badObserve & observe0 <TotalRuns -> (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=1 & badObserve & observe1 <TotalRuns -> (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=2 & badObserve & observe2 <TotalRuns -> (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=3 & badObserve & observe3 <TotalRuns -> (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=4 & badObserve & observe4 <TotalRuns -> (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=5 & badObserve & observe5 <TotalRuns -> (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=6 & badObserve & observe6 <TotalRuns -> (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=7 & badObserve & observe7 <TotalRuns -> (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=8 & badObserve & observe8 <TotalRuns -> (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=9 & badObserve & observe9 <TotalRuns -> (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=10 & badObserve & observe10<TotalRuns -> (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=11 & badObserve & observe11<TotalRuns -> (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=12 & badObserve & observe12<TotalRuns -> (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=13 & badObserve & observe13<TotalRuns -> (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=14 & badObserve & observe14<TotalRuns -> (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=15 & badObserve & observe15<TotalRuns -> (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=16 & badObserve & observe16<TotalRuns -> (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=17 & badObserve & observe17<TotalRuns -> (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=18 & badObserve & observe18<TotalRuns -> (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
- [] lastSeen=19 & badObserve & observe19<TotalRuns -> (observe19'=observe19+1) & (deliver'=true) & (run'=true) & (badObserve'=false);
-
- // RECIPIENT
- // Delivery to destination
- [] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false);
- // Start a newInstance instance
- [] done -> (newInstance'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood);
-
-endmodule
-label "observe0Greater1" = observe0 > 1;
\ No newline at end of file
diff --git a/examples/pdtmc/nand/nand_10-2.pm b/examples/pdtmc/nand/nand_10-2.pm
old mode 100755
new mode 100644
diff --git a/examples/pdtmc/nand/nand_10-3.pm b/examples/pdtmc/nand/nand_10-3.pm
old mode 100755
new mode 100644
diff --git a/examples/pdtmc/nand/nand_10-4.pm b/examples/pdtmc/nand/nand_10-4.pm
old mode 100755
new mode 100644
diff --git a/examples/pdtmc/nand/nand_10-5.pm b/examples/pdtmc/nand/nand_10-5.pm
old mode 100755
new mode 100644
index c7e7fb563..2b1405c2f
--- a/examples/pdtmc/nand/nand_10-5.pm
+++ b/examples/pdtmc/nand/nand_10-5.pm
@@ -62,7 +62,7 @@ module multiplex
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault
- [] s=4 -> true;
+ [] s=4 -> (s'=s);
endmodule
diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp
index 1c06a4ee7..aa3f9d950 100644
--- a/src/modelchecker/reachability/SparseSccModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp
@@ -25,9 +25,9 @@ namespace storm {
static RationalFunction&& simplify(RationalFunction&& value) {
// In the general case, we don't to anything here, but merely return the value. If something else is
// supposed to happen here, the templated function can be specialized for this particular type.
- STORM_LOG_DEBUG("Simplifying " << value << " ... ");
+ STORM_LOG_TRACE("Simplifying " << value << " ... ");
value.simplify();
- STORM_LOG_DEBUG("done.");
+ STORM_LOG_TRACE("done.");
return std::forward<RationalFunction>(value);
}
@@ -117,7 +117,7 @@ namespace storm {
// Then, we recursively treat all SCCs.
auto modelCheckingStart = std::chrono::high_resolution_clock::now();
std::vector<storm::storage::sparse::state_type> entryStateQueue;
- uint_fast64_t maximalDepth = treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0,entryStateQueue);
+ uint_fast64_t maximalDepth = treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0, storm::settings::parametricSettings().getMaximalSccSize(), entryStateQueue);
// If the entry states were to be eliminated last, we need to do so now.
STORM_LOG_DEBUG("Eliminating entry states as a last step.");
@@ -154,11 +154,11 @@ namespace storm {
}
template<typename ValueType>
- uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, std::vector<storm::storage::sparse::state_type>& entryStateQueue) {
+ uint_fast64_t SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue) {
uint_fast64_t maximalDepth = level;
// If the SCCs are large enough, we try to split them further.
- if (scc.getNumberOfSetBits() > SparseSccModelChecker<ValueType>::maximalSccSize) {
+ if (scc.getNumberOfSetBits() > maximalSccSize) {
STORM_LOG_DEBUG("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further.");
// Here, we further decompose the SCC into sub-SCCs.
@@ -199,7 +199,7 @@ namespace storm {
}
// Recursively descend in SCC-hierarchy.
- uint_fast64_t depth = treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, entryStateQueue);
+ uint_fast64_t depth = treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::parametricSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue);
maximalDepth = std::max(maximalDepth, depth);
}
diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h
index f2ca965b0..d624b7e15 100644
--- a/src/modelchecker/reachability/SparseSccModelChecker.h
+++ b/src/modelchecker/reachability/SparseSccModelChecker.h
@@ -37,13 +37,10 @@ namespace storm {
static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> const& filterFormula);
private:
- static uint_fast64_t treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, std::vector<storm::storage::sparse::state_type>& entryStateQueue);
+ static uint_fast64_t treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue);
static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions);
static bool eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions);
-
- static const uint_fast64_t maximalSccSize = 1000;
-
};
} // namespace reachability
diff --git a/src/settings/modules/ParametricSettings.cpp b/src/settings/modules/ParametricSettings.cpp
index 0a5c8b9af..fd66f93ba 100644
--- a/src/settings/modules/ParametricSettings.cpp
+++ b/src/settings/modules/ParametricSettings.cpp
@@ -8,15 +8,22 @@ namespace storm {
const std::string ParametricSettings::moduleName = "parametric";
const std::string ParametricSettings::entryStatesLastOptionName = "entrylast";
+ const std::string ParametricSettings::maximalSccSizeOptionName = "sccsize";
ParametricSettings::ParametricSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.")
+ .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(50).setIsOptional(true).build()).build());
}
bool ParametricSettings::isEliminateEntryStatesLastSet() const {
return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet();
}
+ uint_fast64_t ParametricSettings::getMaximalSccSize() const {
+ return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger();
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/ParametricSettings.h b/src/settings/modules/ParametricSettings.h
index eaf0a6e9c..4a744256c 100644
--- a/src/settings/modules/ParametricSettings.h
+++ b/src/settings/modules/ParametricSettings.h
@@ -26,10 +26,18 @@ namespace storm {
*/
bool isEliminateEntryStatesLastSet() const;
+ /*!
+ * Retrieves the maximal size of an SCC on which state elimination is to be directly applied.
+ *
+ * @return The maximal size of an SCC on which state elimination is to be directly applied.
+ */
+ uint_fast64_t getMaximalSccSize() const;
+
const static std::string moduleName;
private:
const static std::string entryStatesLastOptionName;
+ const static std::string maximalSccSizeOptionName;
};
} // namespace modules
diff --git a/src/storage/expressions/ExpressionEvaluation.h b/src/storage/expressions/ExpressionEvaluation.h
index 1b0056988..7754b98fa 100644
--- a/src/storage/expressions/ExpressionEvaluation.h
+++ b/src/storage/expressions/ExpressionEvaluation.h
@@ -125,7 +125,6 @@ namespace expressions {
virtual void visit(IntegerLiteralExpression const* expression)
{
// mValue = T(typename T::CoeffType(std::to_string(expression->getValue()), 10));
-
mValue = T(expression->getValue());
}
virtual void visit(DoubleLiteralExpression const* expression)
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 354dba208..8bf537a32 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -27,6 +27,7 @@
#include "log4cplus/consoleappender.h"
#include "log4cplus/fileappender.h"
log4cplus::Logger logger;
+log4cplus::Logger printer;
// Headers that provide auxiliary functionality.
#include "src/utility/OsDetection.h"
diff --git a/src/utility/macros.h b/src/utility/macros.h
index a8d75d3c8..8e2a3c5b2 100644
--- a/src/utility/macros.h
+++ b/src/utility/macros.h
@@ -9,10 +9,8 @@
extern log4cplus::Logger logger;
/*!
- * Define the macros STORM_LOG_ASSERT and STORM_LOG_DEBUG to be silent in non-debug mode and log the message in case the condition
- * fails to evaluate to true.
+ * Define the macros STORM_LOG_ASSERT, STORM_LOG_DEBUG and STORM_LOG_TRACE.
*/
-#ifndef NDEBUG
#define STORM_LOG_ASSERT(cond, message) \
{ \
if (!(cond)) { \
@@ -24,10 +22,10 @@ extern log4cplus::Logger logger;
{ \
LOG4CPLUS_DEBUG(logger, message); \
} while (false)
-#else
-#define STORM_LOG_ASSERT(cond, message) /* empty */
-#define STORM_LOG_DEBUG(message) /* empty */
-#endif
+#define STORM_LOG_TRACE(message) \
+{ \
+ LOG4CPLUS_TRACE(logger, message); \
+} while (false)
// Define STORM_LOG_THROW to always throw the exception with the given message if the condition fails to hold.
#define STORM_LOG_THROW(cond, exception, message) \