diff --git a/CHANGELOG.md b/CHANGELOG.md index 626cf37be..955a43520 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,7 +16,7 @@ Version 1.6.x - API: Simulation of prism-models - API: Model-builder takes a callback function to prevent extension of particular actions, prism-to-explicit mapping can be exported - API: Export of dice-formatted expressions -- Prism-language/explicit builder: Allow action names in commands writing to global variables if these clearly do not write to actions. +- Prism-language/explicit builder: Allow action names in commands writing to global variables if these (clearly) do not conflict with assignments of synchronizing commads. - Prism-language: n-ary predicates are supported (e.g., ExactlyOneOf) - Added support for continuous integration with Github Actions. - `storm-pars`: Exploit monotonicity for computing extremal values and parameter space partitioning. diff --git a/resources/examples/testfiles/mdp/die_selection.nm b/resources/examples/testfiles/mdp/die_selection.nm index 17c211622..dac396e0d 100644 --- a/resources/examples/testfiles/mdp/die_selection.nm +++ b/resources/examples/testfiles/mdp/die_selection.nm @@ -1,4 +1,4 @@ -// Knuth's model of a fair die using only fair coins +// Variation to Knuth's model of a fair die using only fair coins mdp module die diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 4c9cb7ba5..7d54bc15f 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -83,6 +83,7 @@ namespace storm { * @tparam ValueType Type of the probabilities in the sparse model * @param model SymbolicModelDescription of the model * @param options Builder options + * @param actionMask An object to restrict which actions are expanded in the builder * @return A builder */ template diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index c0c98b5b0..61ac28de5 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -280,7 +280,7 @@ namespace storm { template storm::json NextStateGenerator::currentStateToJson(bool onlyObservable) const { storm::json result = unpackStateIntoJson(*state, variableInformation, onlyObservable); - extendStateInformation(result,onlyObservable); + extendStateInformation(result); return result; } @@ -291,7 +291,7 @@ namespace storm { template - void NextStateGenerator::extendStateInformation(storm::json&, bool) const { + void NextStateGenerator::extendStateInformation(storm::json&) const { // Intentionally left empty. } diff --git a/src/storm/generator/NextStateGenerator.h b/src/storm/generator/NextStateGenerator.h index 9046922f9..51d272150 100644 --- a/src/storm/generator/NextStateGenerator.h +++ b/src/storm/generator/NextStateGenerator.h @@ -39,14 +39,29 @@ namespace storm { template class NextStateGenerator; + /*! + * Action masks are arguments you can give to the state generator that limit which states are generated. + * + */ template class ActionMask { public: virtual ~ActionMask() = default; + /** + * This method is called to check whether an action should be expanded. + * The current state is obtained from the generator. + * + * @param generator the generator that is to be masked + * @param actionIndex the actionIndex in Prism Programs; i.e. id of actions. + * @return true if the mask allows building the action/edge/command + */ virtual bool query(storm::generator::NextStateGenerator const &generator, uint64_t actionIndex) = 0; }; - + /*! + * A particular instance of the action mask that uses a callback function + * to evaluate whether an action should be expanded. + */ template class StateValuationFunctionMask : public ActionMask { public: @@ -139,7 +154,7 @@ namespace storm { virtual storm::storage::BitVector evaluateObservationLabels(CompressedState const& state) const =0; - virtual void extendStateInformation(storm::json& stateInfo, bool onlyObservable = false) const; + virtual void extendStateInformation(storm::json& stateInfo) const; virtual storm::storage::sparse::StateValuationsBuilder initializeObservationValuationsBuilder() const; diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 88de55e02..26c9bf673 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -793,7 +793,7 @@ namespace storm { } template - void PrismNextStateGenerator::extendStateInformation(storm::json& result, bool onlyObservable) const { + void PrismNextStateGenerator::extendStateInformation(storm::json& result) const { for (uint64_t i = 0; i < program.getNumberOfObservationLabels(); ++i) { result[program.getObservationLabels()[i].getName()] = this->evaluator->asInt(program.getObservationLabels()[i].getStatePredicateExpression()); diff --git a/src/storm/generator/PrismNextStateGenerator.h b/src/storm/generator/PrismNextStateGenerator.h index 7e63da41a..a053e4488 100644 --- a/src/storm/generator/PrismNextStateGenerator.h +++ b/src/storm/generator/PrismNextStateGenerator.h @@ -102,10 +102,10 @@ namespace storm { */ void addLabeledChoices(std::vector>& choices, CompressedState const& state, StateToIdCallback stateToIdCallback, CommandFilter const& commandFilter = CommandFilter::All); - /* + /*! * Extend the Json struct with additional information about the state. */ - virtual void extendStateInformation(storm::json& stateInfo, bool onlyObservable = false) const override; + virtual void extendStateInformation(storm::json& stateInfo) const override; /*! * Evaluate observation labels diff --git a/src/storm/simulator/PrismProgramSimulator.h b/src/storm/simulator/PrismProgramSimulator.h index 99e828bf9..daec0a81e 100644 --- a/src/storm/simulator/PrismProgramSimulator.h +++ b/src/storm/simulator/PrismProgramSimulator.h @@ -39,6 +39,7 @@ namespace storm { /** * * @return A list of choices that encode the possibilities in the current state. + * @note successor states are encoded using state indices that will potentially be invalidated as soon as the internal state of the simulator changes */ std::vector> const& getChoices() const; diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index d41e05de1..5340fab98 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/src/storm/storage/expressions/Expression.cpp @@ -13,7 +13,7 @@ #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/macros.h" -#include "storm/storage/expressions/SimplificationVisitor.h" +#include "storm/storage/expressions/RestrictSyntaxVisitor.h" namespace storm { namespace expressions { @@ -55,7 +55,7 @@ namespace storm { } Expression Expression::substituteNonStandardPredicates() const { - return SimplificationVisitor().substitute(*this); + return RestrictSyntaxVisitor().substitute(*this); } bool Expression::evaluateAsBool(Valuation const* valuation) const { diff --git a/src/storm/storage/expressions/ExpressionStringFormat.h b/src/storm/storage/expressions/ExpressionStringFormat.h deleted file mode 100644 index fc4d7ed8a..000000000 --- a/src/storm/storage/expressions/ExpressionStringFormat.h +++ /dev/null @@ -1,9 +0,0 @@ -#pragma once - -namespace storm { - namespace expressions { - struct ExpressionStringFormat { - bool alternativeIff = false; - }; - } -} \ No newline at end of file diff --git a/src/storm/storage/expressions/ExpressionVisitor.h b/src/storm/storage/expressions/ExpressionVisitor.h index 367178426..877312aed 100644 --- a/src/storm/storage/expressions/ExpressionVisitor.h +++ b/src/storm/storage/expressions/ExpressionVisitor.h @@ -18,7 +18,7 @@ namespace storm { class IntegerLiteralExpression; class RationalLiteralExpression; class PredicateExpression; - + class ExpressionVisitor { public: virtual ~ExpressionVisitor() = default; diff --git a/src/storm/storage/expressions/PredicateExpression.cpp b/src/storm/storage/expressions/PredicateExpression.cpp index 73b9a9e2e..453a776ab 100644 --- a/src/storm/storage/expressions/PredicateExpression.cpp +++ b/src/storm/storage/expressions/PredicateExpression.cpp @@ -26,16 +26,16 @@ namespace storm { bool PredicateExpression::evaluateAsBool(Valuation const *valuation) const { STORM_LOG_THROW(this->hasBooleanType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean."); - storm::storage::BitVector results(operands.size()); - uint64_t i = 0; + uint64_t nrTrue = 0; for(auto const& operand : operands) { - results.set(i, operand->evaluateAsBool(valuation)); - ++i; + if (operand->evaluateAsBool(valuation)) { + nrTrue++; + } } switch(predicate) { - case PredicateType::ExactlyOneOf: return results.getNumberOfSetBits() == 1; - case PredicateType::AtMostOneOf: return results.getNumberOfSetBits() <= 1; - case PredicateType::AtLeastOneOf: return results.getNumberOfSetBits() >= 1; + case PredicateType::ExactlyOneOf: return nrTrue == 1; + case PredicateType::AtMostOneOf: return nrTrue <= 1; + case PredicateType::AtLeastOneOf: return nrTrue >= 1; } STORM_LOG_ASSERT(false, "Unknown predicate type"); } @@ -45,7 +45,14 @@ namespace storm { for (auto const& operand : operands) { simplifiedOperands.push_back(operand->simplify()); } - return std::shared_ptr(new PredicateExpression(this->getManager(), this->getType(), simplifiedOperands, predicate)); + // Return new expression if something changed. + for (uint64_t i = 0; i < operands.size(); ++i) { + if (operands[i] != simplifiedOperands[i]) { + return std::shared_ptr(new PredicateExpression(this->getManager(), this->getType(), simplifiedOperands, predicate)); + } + } + // All operands remained the same. + return this->shared_from_this(); } boost::any PredicateExpression::accept(ExpressionVisitor &visitor, boost::any const &data) const { diff --git a/src/storm/storage/expressions/SimplificationVisitor.cpp b/src/storm/storage/expressions/RestrictSyntaxVisitor.cpp similarity index 91% rename from src/storm/storage/expressions/SimplificationVisitor.cpp rename to src/storm/storage/expressions/RestrictSyntaxVisitor.cpp index 0d4c0a1b0..8c53cd3a0 100644 --- a/src/storm/storage/expressions/SimplificationVisitor.cpp +++ b/src/storm/storage/expressions/RestrictSyntaxVisitor.cpp @@ -2,23 +2,23 @@ #include #include -#include "storm/storage/expressions/SimplificationVisitor.h" +#include "storm/storage/expressions/RestrictSyntaxVisitor.h" #include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/PredicateExpression.h" #include "storm/storage/expressions/ExpressionManager.h" namespace storm { namespace expressions { - SimplificationVisitor::SimplificationVisitor() { + RestrictSyntaxVisitor::RestrictSyntaxVisitor() { // Intentionally left empty. } - Expression SimplificationVisitor::substitute(Expression const &expression) { + Expression RestrictSyntaxVisitor::substitute(Expression const &expression) { return Expression(boost::any_cast>( expression.getBaseExpression().accept(*this, boost::none))); } - boost::any SimplificationVisitor::visit(IfThenElseExpression const &expression, boost::any const &data) { + boost::any RestrictSyntaxVisitor::visit(IfThenElseExpression const &expression, boost::any const &data) { std::shared_ptr conditionExpression = boost::any_cast>( expression.getCondition()->accept(*this, data)); std::shared_ptr thenExpression = boost::any_cast>( @@ -39,7 +39,7 @@ namespace storm { } boost::any - SimplificationVisitor::visit(BinaryBooleanFunctionExpression const &expression, boost::any const &data) { + RestrictSyntaxVisitor::visit(BinaryBooleanFunctionExpression const &expression, boost::any const &data) { std::shared_ptr firstExpression = boost::any_cast>( expression.getFirstOperand()->accept(*this, data)); std::shared_ptr secondExpression = boost::any_cast>( @@ -58,7 +58,7 @@ namespace storm { } boost::any - SimplificationVisitor::visit(BinaryNumericalFunctionExpression const &expression, boost::any const &data) { + RestrictSyntaxVisitor::visit(BinaryNumericalFunctionExpression const &expression, boost::any const &data) { std::shared_ptr firstExpression = boost::any_cast>( expression.getFirstOperand()->accept(*this, data)); std::shared_ptr secondExpression = boost::any_cast>( @@ -76,7 +76,7 @@ namespace storm { } } - boost::any SimplificationVisitor::visit(BinaryRelationExpression const &expression, boost::any const &data) { + boost::any RestrictSyntaxVisitor::visit(BinaryRelationExpression const &expression, boost::any const &data) { std::shared_ptr firstExpression = boost::any_cast>( expression.getFirstOperand()->accept(*this, data)); std::shared_ptr secondExpression = boost::any_cast>( @@ -93,14 +93,14 @@ namespace storm { } } - boost::any SimplificationVisitor::visit(VariableExpression const &expression, boost::any const &) { + boost::any RestrictSyntaxVisitor::visit(VariableExpression const &expression, boost::any const &) { return expression.getSharedPointer(); } boost::any - SimplificationVisitor::visit(UnaryBooleanFunctionExpression const &expression, boost::any const &data) { + RestrictSyntaxVisitor::visit(UnaryBooleanFunctionExpression const &expression, boost::any const &data) { std::shared_ptr operandExpression = boost::any_cast>( expression.getOperand()->accept(*this, data)); @@ -115,7 +115,7 @@ namespace storm { } boost::any - SimplificationVisitor::visit(UnaryNumericalFunctionExpression const &expression, boost::any const &data) { + RestrictSyntaxVisitor::visit(UnaryNumericalFunctionExpression const &expression, boost::any const &data) { std::shared_ptr operandExpression = boost::any_cast>( expression.getOperand()->accept(*this, data)); @@ -129,7 +129,7 @@ namespace storm { } } - boost::any SimplificationVisitor::visit(PredicateExpression const &expression, boost::any const &data) { + boost::any RestrictSyntaxVisitor::visit(PredicateExpression const &expression, boost::any const &data) { std::vector newExpressions; for (uint64_t i = 0; i < expression.getArity(); ++i) { newExpressions.emplace_back(boost::any_cast>( @@ -155,15 +155,15 @@ namespace storm { } - boost::any SimplificationVisitor::visit(BooleanLiteralExpression const &expression, boost::any const &) { + boost::any RestrictSyntaxVisitor::visit(BooleanLiteralExpression const &expression, boost::any const &) { return expression.getSharedPointer(); } - boost::any SimplificationVisitor::visit(IntegerLiteralExpression const &expression, boost::any const &) { + boost::any RestrictSyntaxVisitor::visit(IntegerLiteralExpression const &expression, boost::any const &) { return expression.getSharedPointer(); } - boost::any SimplificationVisitor::visit(RationalLiteralExpression const &expression, boost::any const &) { + boost::any RestrictSyntaxVisitor::visit(RationalLiteralExpression const &expression, boost::any const &) { return expression.getSharedPointer(); } diff --git a/src/storm/storage/expressions/SimplificationVisitor.h b/src/storm/storage/expressions/RestrictSyntaxVisitor.h similarity index 95% rename from src/storm/storage/expressions/SimplificationVisitor.h rename to src/storm/storage/expressions/RestrictSyntaxVisitor.h index b1c80314e..2b0041b7a 100644 --- a/src/storm/storage/expressions/SimplificationVisitor.h +++ b/src/storm/storage/expressions/RestrictSyntaxVisitor.h @@ -6,7 +6,7 @@ namespace storm { namespace expressions { - class SimplificationVisitor : public ExpressionVisitor { + class RestrictSyntaxVisitor : public ExpressionVisitor { public: /*! * Creates a new simplification visitor that replaces predicates by other (simpler?) predicates. @@ -15,7 +15,7 @@ namespace storm { * Currently, the visitor only replaces nonstandard predicates * */ - SimplificationVisitor(); + RestrictSyntaxVisitor(); /*! * Simplifies based on the configuration. diff --git a/src/storm/storage/expressions/ToDiceStringVisitor.cpp b/src/storm/storage/expressions/ToDiceStringVisitor.cpp index 2a9467cc3..c07bab032 100644 --- a/src/storm/storage/expressions/ToDiceStringVisitor.cpp +++ b/src/storm/storage/expressions/ToDiceStringVisitor.cpp @@ -1,5 +1,6 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/storage/expressions/ToDiceStringVisitor.h" +#include "storm/storage/expressions/Expressions.h" namespace storm { namespace expressions { diff --git a/src/storm/storage/expressions/ToDiceStringVisitor.h b/src/storm/storage/expressions/ToDiceStringVisitor.h index 00a91d7f9..9c04b4d3b 100644 --- a/src/storm/storage/expressions/ToDiceStringVisitor.h +++ b/src/storm/storage/expressions/ToDiceStringVisitor.h @@ -3,7 +3,6 @@ #include #include "storm/storage/expressions/Expression.h" -#include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/ExpressionVisitor.h" namespace storm { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 363ee9375..afca86cb4 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -6,8 +6,8 @@ #include #include #include -#include +#include "storm/storage/BitVector.h" #include "storm/storage/prism/Constant.h" #include "storm/storage/prism/Formula.h" #include "storm/storage/prism/Label.h" @@ -739,6 +739,10 @@ namespace storm { */ std::pair> toJani(std::vector const& properties, bool allVariablesGlobal = true, std::string suffix = "") const; + /*! + * Compute the (labelled) commands in the program that may be synchronizing + * @return A bitvector representing the set of commands by global command index + */ storm::storage::BitVector const& getPossiblySynchronizingCommands() const; private: