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

Added and fixed some example models. Added option for maximal size of SCC that gets eliminated using state elimination. 

Former-commit-id: bf1e73ff61
tempestpy_adaptions
dehnert 10 years ago
parent
4eea90646a
commit
0776d8a74b
12 changed files with 29 additions and 210 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 191
      examples/pdtmc/crowds/crowds3_5.pm
  2. 0
      examples/pdtmc/nand/nand_10-2.pm
  3. 0
      examples/pdtmc/nand/nand_10-3.pm
  4. 0
      examples/pdtmc/nand/nand_10-4.pm
  5. 2
      examples/pdtmc/nand/nand_10-5.pm
  6. 12
      src/modelchecker/reachability/SparseSccModelChecker.cpp
  7. 5
      src/modelchecker/reachability/SparseSccModelChecker.h
  8. 7
      src/settings/modules/ParametricSettings.cpp
  9. 8
      src/settings/modules/ParametricSettings.h
  10. 1
      src/storage/expressions/ExpressionEvaluation.h
  11. 1
      src/utility/cli.h
  12. 12
      src/utility/macros.h

191
examples/pdtmc/crowds/crowds3_5.pm
View File

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

0
examples/pdtmc/nand/nand_10-2.pm
View File

0
examples/pdtmc/nand/nand_10-3.pm
View File

0
examples/pdtmc/nand/nand_10-4.pm
View File

2
examples/pdtmc/nand/nand_10-5.pm
View File

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

12
src/modelchecker/reachability/SparseSccModelChecker.cpp
View File

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

5
src/modelchecker/reachability/SparseSccModelChecker.h
View File

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

7
src/settings/modules/ParametricSettings.cpp
View File

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

8
src/settings/modules/ParametricSettings.h
View File

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

1
src/storage/expressions/ExpressionEvaluation.h
View File

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

1
src/utility/cli.h
View File

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

12
src/utility/macros.h
View File

@ -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) \

Write Preview
Loading…
Cancel
Save