diff --git a/src/adapters/IntermediateRepresentationAdapter.h b/src/adapters/IntermediateRepresentationAdapter.h index fad0217ad..6c5774bfc 100644 --- a/src/adapters/IntermediateRepresentationAdapter.h +++ b/src/adapters/IntermediateRepresentationAdapter.h @@ -9,6 +9,7 @@ #define STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ #include "src/storage/SparseMatrix.h" +#include "src/utility/Settings.h" #include #include @@ -19,6 +20,10 @@ typedef std::pair, std::vector> StateType; +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + namespace storm { namespace adapters { @@ -48,7 +53,7 @@ class IntermediateRepresentationAdapter { public: template static storm::storage::SparseMatrix* toSparseMatrix(storm::ir::Program const& program) { - + LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program."); uint_fast64_t numberOfIntegerVariables = 0; uint_fast64_t numberOfBooleanVariables = 0; for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { @@ -108,6 +113,8 @@ public: StateType* currentState = stateQueue.front(); stateQueue.pop(); + bool hasTransition = false; + // Iterate over all modules. for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { storm::ir::Module const& module = program.getModule(i); @@ -118,21 +125,27 @@ public: // Check if this command is enabled in the current state. if (command.getGuard()->getValueAsBool(*currentState)) { + hasTransition = true; std::unordered_map stateToProbabilityMap; + std::queue statesToDelete; for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { storm::ir::Update const& update = command.getUpdate(k); StateType* newState = new StateType(*currentState); - + // std::cout << "took state: " << newState->first << "/" << newState->second << std::endl; std::map const& booleanAssignmentMap = update.getBooleanAssignments(); for (auto assignedVariable : booleanAssignmentMap) { setValue(newState, booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(*currentState)); } std::map const& integerAssignmentMap = update.getIntegerAssignments(); for (auto assignedVariable : integerAssignmentMap) { + // std::cout << "evaluting " << assignedVariable.second.getExpression()->toString() << " as " << assignedVariable.second.getExpression()->getValueAsInt(*currentState) << std::endl; setValue(newState, integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(*currentState)); } + // std::cout << "applied: " << update.toString() << std::endl; + // std::cout << "got: " << newState->first << "/" << newState->second << std::endl; + auto probIt = stateToProbabilityMap.find(newState); if (probIt != stateToProbabilityMap.end()) { stateToProbabilityMap[newState] += update.getLikelihoodExpression()->getValueAsDouble(*currentState); @@ -144,7 +157,7 @@ public: auto it = stateToIndexMap.find(newState); if (it != stateToIndexMap.end()) { // Delete the state object directly as we have already seen that state. - delete newState; + statesToDelete.push(newState); } else { // Add state to the queue of states that are still to be explored. stateQueue.push(newState); @@ -157,18 +170,31 @@ public: ++nextIndex; } } + while (!statesToDelete.empty()) { + delete statesToDelete.front(); + statesToDelete.pop(); + } } } } - } - std::cout << "Found " << allStates.size() << " reachable states and " << totalNumberOfTransitions << " transitions."; + if (!hasTransition) { + if (storm::settings::instance()->isSet("fix-deadlocks")) { + ++totalNumberOfTransitions; + } else { + LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state."); + throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state."; + } + } + } storm::storage::SparseMatrix* resultMatrix = new storm::storage::SparseMatrix(allStates.size()); resultMatrix->initialize(totalNumberOfTransitions); uint_fast64_t currentIndex = 0; for (StateType* currentState : allStates) { + bool hasTransition = false; + // Iterate over all modules. for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { storm::ir::Module const& module = program.getModule(i); @@ -179,6 +205,7 @@ public: // Check if this command is enabled in the current state. if (command.getGuard()->getValueAsBool(*currentState)) { + hasTransition = true; std::map stateIndexToProbabilityMap; for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { storm::ir::Update const& update = command.getUpdate(k); @@ -212,15 +239,22 @@ public: } } } + if (!hasTransition) { + resultMatrix->addNextValue(currentIndex, currentIndex, 1); + } + ++currentIndex; } resultMatrix->finalize(); + LOG4CPLUS_INFO(logger, "Created sparse matrix with " << allStates.size() << " reachable states and " << totalNumberOfTransitions << " transitions."); + // Now free all the elements we allocated. for (auto element : allStates) { delete element; } + return resultMatrix; } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 19027a3f8..78795388e 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -88,7 +88,7 @@ struct PrismParser::PrismGrammar : qi::grammar> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; integerMultExpression.name("integer expression"); - integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS))]]; integerPlusExpression.name("integer expression"); integerExpression %= integerPlusExpression; integerExpression.name("integer expression"); @@ -98,7 +98,7 @@ struct PrismParser::PrismGrammar : qi::grammar> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; constantIntegerMultExpression.name("constant integer expression"); - constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS))]]; constantIntegerPlusExpression.name("constant integer expression"); constantIntegerExpression %= constantIntegerPlusExpression; constantIntegerExpression.name("constant integer expression"); @@ -106,9 +106,9 @@ struct PrismParser::PrismGrammar : qi::grammar> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); constantAtomicDoubleExpression.name("constant double expression"); - constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> constantAtomicDoubleExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::DIVIDE))]]; constantDoubleMultExpression.name("constant double expression"); - constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS))]]; constantDoublePlusExpression.name("constant double expression"); constantDoubleExpression %= constantDoublePlusExpression; constantDoubleExpression.name("constant double expression"); @@ -186,9 +186,9 @@ struct PrismParser::PrismGrammar : qi::grammar> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::val(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::val(nextBooleanVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::bool_, phoenix::val(nextBooleanVariableIndex), qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), phoenix::ref(nextBooleanVariableIndex)++]; + booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextBooleanVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::bool_, phoenix::ref(nextBooleanVariableIndex), qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), phoenix::ref(nextBooleanVariableIndex) = phoenix::ref(nextBooleanVariableIndex) + 1]; booleanVariableDefinition.name("boolean variable declaration"); - integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::val(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::val(nextIntegerVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, phoenix::val(nextIntegerVariableIndex), qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex)++]; + integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextIntegerVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1]; integerVariableDefinition.name("integer variable declaration"); variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); variableDefinition.name("variable declaration"); @@ -297,18 +297,18 @@ struct PrismParser::PrismGrammar : qi::grammar(), Skipper> integerExpression; - qi::rule(), Skipper> integerPlusExpression; + qi::rule(), qi::locals, Skipper> integerPlusExpression; qi::rule(), Skipper> integerMultExpression; qi::rule(), Skipper> atomicIntegerExpression; qi::rule(), Skipper> constantIntegerExpression; - qi::rule(), Skipper> constantIntegerPlusExpression; + qi::rule(), qi::locals, Skipper> constantIntegerPlusExpression; qi::rule(), Skipper> constantIntegerMultExpression; qi::rule(), Skipper> constantAtomicIntegerExpression; // Rules with double result type. qi::rule(), Skipper> constantDoubleExpression; - qi::rule(), Skipper> constantDoublePlusExpression; - qi::rule(), Skipper> constantDoubleMultExpression; + qi::rule(), qi::locals, Skipper> constantDoublePlusExpression; + qi::rule(), qi::locals, Skipper> constantDoubleMultExpression; qi::rule(), Skipper> constantAtomicDoubleExpression; // Rules for variable recognition. diff --git a/src/storm.cpp b/src/storm.cpp index dfb2109e5..b34529d94 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -198,7 +198,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast6 storm::formula::BoundedUntil* boundedUntilFormula = new storm::formula::BoundedUntil(new storm::formula::Ap("true"), electedFormula, 1); probFormula = new storm::formula::ProbabilisticNoBoundOperator(boundedUntilFormula); - for (uint_fast64_t L = 1; L < 5; ++L) { + for (uint_fast64_t L = 9; L < 10; ++L) { boundedUntilFormula->setBound(L*(n + 1)); mc->check(*probFormula); } @@ -224,12 +224,11 @@ void testChecking() { if (parser.getType() == storm::models::DTMC) { std::shared_ptr> dtmc = parser.getModel>(); dtmc->printModelInformationToStream(std::cout); + // testCheckingDie(*dtmc); + // testCheckingCrowds(*dtmc); + testCheckingSynchronousLeader(*dtmc, 5); } else std::cout << "Input is not DTMC" << std::endl; - - // testCheckingDie(*dtmc); - // testCheckingCrowds(*dtmc); - // testCheckingSynchronousLeader(*dtmc, 4); } /*! @@ -237,9 +236,9 @@ void testChecking() { */ int main(const int argc, const char* argv[]) { initializeLogger(); - // if (!parseOptions(argc, argv)) { - // return 0; - //} + if (!parseOptions(argc, argv)) { + return 0; + } // printHeader(argc, argv); // testChecking(); @@ -247,7 +246,7 @@ int main(const int argc, const char* argv[]) { storm::parser::PrismParser parser; std::shared_ptr program = parser.parseFile("test.input"); storm::storage::SparseMatrix* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix(*program); - result->print(); + // result->print(); delete result; cleanUp(); diff --git a/test.input b/test.input index 700951a05..522d107da 100644 --- a/test.input +++ b/test.input @@ -1,24 +1,89 @@ -// Knuth's model of a fair die using only fair coins dtmc -module die - - // local state - s : [0..7] init 0; - // value of the dice - d : [0..6] init 0; - - [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); - [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); - [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); - [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); - [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); - [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); - [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); - [] s=7 -> 1: (s'=7); - +// probability of forwarding +const double PF = 0.8; +const double notPF = .2; // must be 1-PF +// probability that a crowd member is bad +const double badC = .167; + // probability that a crowd member is good +const double goodC = 0.833; +// Total number of protocol runs to analyze +const int TotalRuns = 5; +// size of the crowd +const int CrowdSize = 10; + +module crowds + // protocol phase + phase: [0..4] init 0; + + // crowd member good (or bad) + good: bool init false; + + // number of protocol runs + runCount: [0..TotalRuns] init 0; + + // observe_i is the number of times the attacker observed crowd member i + observe0: [0..TotalRuns] init 0; + + observe1: [0..TotalRuns] init 0; + + observe2: [0..TotalRuns] init 0; + + observe3: [0..TotalRuns] init 0; + + observe4: [0..TotalRuns] init 0; + + observe5: [0..TotalRuns] init 0; + + observe6: [0..TotalRuns] init 0; + + observe7: [0..TotalRuns] init 0; + + observe8: [0..TotalRuns] init 0; + + observe9: [0..TotalRuns] init 0; + + // the last seen crowd member + lastSeen: [0..CrowdSize - 1] init 0; + + // get the protocol started + [] phase=0 & runCount 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + + // decide whether crowd member is good or bad according to given probabilities + [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); + + // if the current member is a good member, update the last seen index (chosen uniformly) + [] phase=2 & good -> 1/10 : (lastSeen'=0) & (phase'=3) + 1/10 : (lastSeen'=1) & (phase'=3) + 1/10 : (lastSeen'=2) & (phase'=3) + 1/10 : (lastSeen'=3) & (phase'=3) + 1/10 : (lastSeen'=4) & (phase'=3) + 1/10 : (lastSeen'=5) & (phase'=3) + 1/10 : (lastSeen'=6) & (phase'=3) + 1/10 : (lastSeen'=7) & (phase'=3) + 1/10 : (lastSeen'=8) & (phase'=3) + 1/10 : (lastSeen'=9) & (phase'=3); + + // if the current member is a bad member, record the most recently seen index + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); + [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4); + [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4); + [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4); + [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4); + [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (observe9'=observe9+1) & (phase'=4); + + // good crowd members forward with probability PF and deliver otherwise + [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); + + // deliver the message and start over + [] phase=4 -> 1: (phase'=0); + endmodule -rewards "coin_flips" - [] s<7 : 1; -endrewards +label "observe0Greater1" = observe0>1; +label "observe1Greater1" = observe1>1; +label "observe2Greater1" = observe2>1; +label "observe3Greater1" = observe3>1; +label "observe4Greater1" = observe4>1; +label "observe5Greater1" = observe5>1; +label "observe6Greater1" = observe6>1; +label "observe7Greater1" = observe7>1; +label "observe8Greater1" = observe8>1; +label "observe9Greater1" = observe9>1; +label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1|observe5>1|observe6>1|observe7>1|observe8>1|observe9>1; +label "observeOnlyTrueSender" = observe0>1&observe1<=1&observe2<=1&observe3<=1&observe4<=1&observe5<=1&observe6<=1&observe7<=1&observe8<=1&observe9<=1; \ No newline at end of file