From 5f120fd5bbdccb77e4df1fd0279b5e9a470598a4 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 25 Apr 2017 17:36:37 +0200 Subject: [PATCH 1/7] Fixed enabling CLN when there is no system version of carl --- resources/3rdparty/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index e917be668..cd6b24ff4 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -213,7 +213,7 @@ if(USE_CARL) message("START CARL CONFIG PROCESS") file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) execute_process( - COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON" + COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DCARL_USE_CLN_NUMBERS=ON" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON" WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download OUTPUT_VARIABLE carlconfig_out RESULT_VARIABLE carlconfig_result) From 586929ea64b07ace50674353722cbec33ac58f61 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 24 Apr 2017 13:27:19 +0200 Subject: [PATCH 2/7] As we do not support windows, we can also get rid of: #ifndef WINDOWS especially since the guards were around move-constructors, which are supported under Windows since Visual Studio 2015 --- src/storm/models/sparse/Ctmc.h | 4 +--- src/storm/models/sparse/DeterministicModel.h | 5 ++--- src/storm/models/sparse/Dtmc.h | 4 +--- src/storm/models/sparse/MarkovAutomaton.h | 4 +--- src/storm/models/sparse/Mdp.h | 4 +--- src/storm/models/sparse/Model.h | 6 +----- src/storm/models/sparse/NondeterministicModel.h | 4 +--- src/storm/models/sparse/StandardRewardModel.h | 4 +--- src/storm/models/sparse/StochasticTwoPlayerGame.h | 4 +--- src/storm/storage/expressions/BaseExpression.h | 4 +--- .../storage/expressions/BinaryBooleanFunctionExpression.h | 3 +-- src/storm/storage/expressions/BinaryExpression.h | 3 +-- .../storage/expressions/BinaryNumericalFunctionExpression.h | 3 +-- src/storm/storage/expressions/BinaryRelationExpression.h | 3 +-- src/storm/storage/expressions/BooleanLiteralExpression.h | 3 +-- src/storm/storage/expressions/Expression.h | 4 +--- src/storm/storage/expressions/IfThenElseExpression.h | 3 +-- src/storm/storage/expressions/IntegerLiteralExpression.h | 3 +-- src/storm/storage/expressions/LinearCoefficientVisitor.h | 4 +--- src/storm/storage/expressions/RationalLiteralExpression.h | 3 +-- .../storage/expressions/UnaryBooleanFunctionExpression.h | 2 -- src/storm/storage/expressions/UnaryExpression.h | 2 -- .../storage/expressions/UnaryNumericalFunctionExpression.h | 3 +-- src/storm/storage/expressions/Variable.h | 3 +-- src/storm/storage/expressions/VariableExpression.h | 3 +-- src/storm/storage/prism/Assignment.h | 4 +--- src/storm/storage/prism/BooleanVariable.h | 2 -- src/storm/storage/prism/Command.h | 4 +--- src/storm/storage/prism/Constant.h | 4 +--- src/storm/storage/prism/Formula.h | 4 +--- src/storm/storage/prism/InitialConstruct.h | 4 +--- src/storm/storage/prism/IntegerVariable.h | 2 -- src/storm/storage/prism/Label.h | 4 +--- src/storm/storage/prism/LocatedInformation.h | 4 +--- src/storm/storage/prism/Module.h | 4 +--- src/storm/storage/prism/Program.h | 4 +--- src/storm/storage/prism/RewardModel.h | 4 +--- src/storm/storage/prism/StateActionReward.h | 4 +--- src/storm/storage/prism/StateReward.h | 4 +--- src/storm/storage/prism/SystemCompositionConstruct.h | 4 +--- src/storm/storage/prism/TransitionReward.h | 4 +--- src/storm/storage/prism/Update.h | 4 +--- src/storm/storage/prism/Variable.h | 4 +--- 43 files changed, 40 insertions(+), 116 deletions(-) diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index 8bb1f37ed..3bf6dc78c 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -54,11 +54,9 @@ namespace storm { Ctmc(Ctmc const& ctmc) = default; Ctmc& operator=(Ctmc const& ctmc) = default; - -#ifndef WINDOWS Ctmc(Ctmc&& ctmc) = default; Ctmc& operator=(Ctmc&& ctmc) = default; -#endif + /*! * Retrieves the vector of exit rates of the model. * diff --git a/src/storm/models/sparse/DeterministicModel.h b/src/storm/models/sparse/DeterministicModel.h index a7a2503de..c823b91cf 100644 --- a/src/storm/models/sparse/DeterministicModel.h +++ b/src/storm/models/sparse/DeterministicModel.h @@ -47,11 +47,10 @@ namespace storm { DeterministicModel(DeterministicModel const& other) = default; DeterministicModel& operator=(DeterministicModel const& other) = default; -#ifndef WINDOWS + DeterministicModel(DeterministicModel&& other) = default; DeterministicModel& operator=(DeterministicModel&& model) = default; -#endif - + virtual void reduceToStateBasedRewards() override; virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; diff --git a/src/storm/models/sparse/Dtmc.h b/src/storm/models/sparse/Dtmc.h index c5b4a4420..25002856c 100644 --- a/src/storm/models/sparse/Dtmc.h +++ b/src/storm/models/sparse/Dtmc.h @@ -44,11 +44,9 @@ namespace storm { Dtmc(Dtmc const& dtmc) = default; Dtmc& operator=(Dtmc const& dtmc) = default; -#ifndef WINDOWS Dtmc(Dtmc&& dtmc) = default; Dtmc& operator=(Dtmc&& dtmc) = default; -#endif - + #ifdef STORM_HAVE_CARL class ConstraintCollector { diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index 477d0ee5f..5e1cb7862 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -107,11 +107,9 @@ namespace storm { MarkovAutomaton(MarkovAutomaton const& other) = default; MarkovAutomaton& operator=(MarkovAutomaton const& other) = default; -#ifndef WINDOWS MarkovAutomaton(MarkovAutomaton&& other) = default; MarkovAutomaton& operator=(MarkovAutomaton&& other) = default; -#endif - + /*! * Retrieves whether the Markov automaton is closed. * diff --git a/src/storm/models/sparse/Mdp.h b/src/storm/models/sparse/Mdp.h index 5651d5dc9..ba231cd72 100644 --- a/src/storm/models/sparse/Mdp.h +++ b/src/storm/models/sparse/Mdp.h @@ -44,11 +44,9 @@ namespace storm { Mdp(Mdp const& other) = default; Mdp& operator=(Mdp const& other) = default; -#ifndef WINDOWS Mdp(Mdp&& other) = default; Mdp& operator=(Mdp&& other) = default; -#endif - + /*! * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones * whose label set is contained in the given label set. Note that is is only valid to call this method diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index a545ae3ce..206b364b7 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -46,11 +46,7 @@ namespace storm { Model(Model const& other) = default; Model& operator=(Model const& other) = default; -#ifndef WINDOWS - Model(Model&& other) = default; - Model& operator=(Model&& other) = default; -#endif - + /*! * Constructs a model from the given data. * diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index 8d0960aa5..b0f32e688 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -47,11 +47,9 @@ namespace storm { NondeterministicModel(NondeterministicModel const& other) = default; NondeterministicModel& operator=(NondeterministicModel const& other) = default; -#ifndef WINDOWS NondeterministicModel(NondeterministicModel&& other) = default; NondeterministicModel& operator=(NondeterministicModel&& other) = default; -#endif - + /*! * Retrieves the number of (nondeterministic) choices in the model. * diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index e98430d64..57b0d5c5a 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -40,11 +40,9 @@ namespace storm { StandardRewardModel(StandardRewardModel const& dtmc) = default; StandardRewardModel& operator=(StandardRewardModel const& dtmc) = default; -#ifndef WINDOWS StandardRewardModel(StandardRewardModel&& dtmc) = default; StandardRewardModel& operator=(StandardRewardModel&& dtmc) = default; -#endif - + /*! * Retrieves whether the reward model has state rewards. * diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.h b/src/storm/models/sparse/StochasticTwoPlayerGame.h index 520001e95..a589decc1 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.h +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.h @@ -52,11 +52,9 @@ namespace storm { StochasticTwoPlayerGame(StochasticTwoPlayerGame const& other) = default; StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame const& other) = default; -#ifndef WINDOWS StochasticTwoPlayerGame(StochasticTwoPlayerGame&& other) = default; StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame&& other) = default; -#endif - + /*! * Retrieves the matrix representing the choices in player 1 states. * diff --git a/src/storm/storage/expressions/BaseExpression.h b/src/storm/storage/expressions/BaseExpression.h index 83c76f7ae..5f93766a5 100644 --- a/src/storm/storage/expressions/BaseExpression.h +++ b/src/storm/storage/expressions/BaseExpression.h @@ -48,11 +48,9 @@ namespace storm { // Create default versions of constructors and assignments. BaseExpression(BaseExpression const&) = default; BaseExpression& operator=(BaseExpression const&) = delete; -#ifndef WINDOWS BaseExpression(BaseExpression&&) = default; BaseExpression& operator=(BaseExpression&&) = delete; -#endif - + // Make the destructor virtual (to allow destruction via base class pointer) and default it. virtual ~BaseExpression() = default; diff --git a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h index eb1344262..5de256e98 100644 --- a/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h +++ b/src/storm/storage/expressions/BinaryBooleanFunctionExpression.h @@ -27,10 +27,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& other) = default; BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression const& other) = delete; -#ifndef WINDOWS BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression&&) = default; BinaryBooleanFunctionExpression& operator=(BinaryBooleanFunctionExpression&&) = delete; -#endif + virtual ~BinaryBooleanFunctionExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/BinaryExpression.h b/src/storm/storage/expressions/BinaryExpression.h index 2ad23e808..2a7eb10bb 100644 --- a/src/storm/storage/expressions/BinaryExpression.h +++ b/src/storm/storage/expressions/BinaryExpression.h @@ -24,10 +24,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. BinaryExpression(BinaryExpression const& other) = default; BinaryExpression& operator=(BinaryExpression const& other) = delete; -#ifndef WINDOWS BinaryExpression(BinaryExpression&&) = default; BinaryExpression& operator=(BinaryExpression&&) = delete; -#endif + virtual ~BinaryExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h index b69c3b8c5..1e9adb028 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.h @@ -27,10 +27,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& other) = default; BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression const& other) = delete; -#ifndef WINDOWS BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression&&) = default; BinaryNumericalFunctionExpression& operator=(BinaryNumericalFunctionExpression&&) = delete; -#endif + virtual ~BinaryNumericalFunctionExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/BinaryRelationExpression.h b/src/storm/storage/expressions/BinaryRelationExpression.h index a9ed11924..b87fe55ef 100644 --- a/src/storm/storage/expressions/BinaryRelationExpression.h +++ b/src/storm/storage/expressions/BinaryRelationExpression.h @@ -27,10 +27,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. BinaryRelationExpression(BinaryRelationExpression const& other) = default; BinaryRelationExpression& operator=(BinaryRelationExpression const& other) = default; -#ifndef WINDOWS BinaryRelationExpression(BinaryRelationExpression&&) = default; BinaryRelationExpression& operator=(BinaryRelationExpression&&) = default; -#endif + virtual ~BinaryRelationExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/BooleanLiteralExpression.h b/src/storm/storage/expressions/BooleanLiteralExpression.h index b989493d0..f87246a30 100644 --- a/src/storm/storage/expressions/BooleanLiteralExpression.h +++ b/src/storm/storage/expressions/BooleanLiteralExpression.h @@ -19,10 +19,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. BooleanLiteralExpression(BooleanLiteralExpression const& other) = default; BooleanLiteralExpression& operator=(BooleanLiteralExpression const& other) = delete; -#ifndef WINDOWS BooleanLiteralExpression(BooleanLiteralExpression&&) = default; BooleanLiteralExpression& operator=(BooleanLiteralExpression&&) = delete; -#endif + virtual ~BooleanLiteralExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index d694017a7..26d6033c6 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -76,11 +76,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. Expression(Expression const& other) = default; Expression& operator=(Expression const& other) = default; -#ifndef WINDOWS Expression(Expression&&) = default; Expression& operator=(Expression&&) = default; -#endif - + /*! * Converts the expression to an expression over the variables of the provided expression manager. */ diff --git a/src/storm/storage/expressions/IfThenElseExpression.h b/src/storm/storage/expressions/IfThenElseExpression.h index 0d1be1d4b..c52c23087 100644 --- a/src/storm/storage/expressions/IfThenElseExpression.h +++ b/src/storm/storage/expressions/IfThenElseExpression.h @@ -21,10 +21,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. IfThenElseExpression(IfThenElseExpression const& other) = default; IfThenElseExpression& operator=(IfThenElseExpression const& other) = delete; -#ifndef WINDOWS IfThenElseExpression(IfThenElseExpression&&) = default; IfThenElseExpression& operator=(IfThenElseExpression&&) = delete; -#endif + virtual ~IfThenElseExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/IntegerLiteralExpression.h b/src/storm/storage/expressions/IntegerLiteralExpression.h index 9266ea968..1a981464f 100644 --- a/src/storm/storage/expressions/IntegerLiteralExpression.h +++ b/src/storm/storage/expressions/IntegerLiteralExpression.h @@ -19,10 +19,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. IntegerLiteralExpression(IntegerLiteralExpression const& other) = default; IntegerLiteralExpression& operator=(IntegerLiteralExpression const& other) = delete; -#ifndef WINDOWS IntegerLiteralExpression(IntegerLiteralExpression&&) = default; IntegerLiteralExpression& operator=(IntegerLiteralExpression&&) = delete; -#endif + virtual ~IntegerLiteralExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/LinearCoefficientVisitor.h b/src/storm/storage/expressions/LinearCoefficientVisitor.h index c5111beab..1a6a14d30 100644 --- a/src/storm/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storm/storage/expressions/LinearCoefficientVisitor.h @@ -18,11 +18,9 @@ namespace storm { VariableCoefficients(VariableCoefficients const& other) = default; VariableCoefficients& operator=(VariableCoefficients const& other) = default; -#ifndef WINDOWS VariableCoefficients(VariableCoefficients&& other) = default; VariableCoefficients& operator=(VariableCoefficients&& other) = default; -#endif - + VariableCoefficients& operator+=(VariableCoefficients&& other); VariableCoefficients& operator-=(VariableCoefficients&& other); VariableCoefficients& operator*=(VariableCoefficients&& other); diff --git a/src/storm/storage/expressions/RationalLiteralExpression.h b/src/storm/storage/expressions/RationalLiteralExpression.h index 77d8f3703..b89505471 100644 --- a/src/storm/storage/expressions/RationalLiteralExpression.h +++ b/src/storm/storage/expressions/RationalLiteralExpression.h @@ -37,10 +37,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. RationalLiteralExpression(RationalLiteralExpression const& other) = default; RationalLiteralExpression& operator=(RationalLiteralExpression const& other) = delete; -#ifndef WINDOWS RationalLiteralExpression(RationalLiteralExpression&&) = default; RationalLiteralExpression& operator=(RationalLiteralExpression&&) = delete; -#endif + virtual ~RationalLiteralExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h index 918300d93..64a185430 100644 --- a/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h +++ b/src/storm/storage/expressions/UnaryBooleanFunctionExpression.h @@ -26,10 +26,8 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& other) = default; UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression const& other) = delete; -#ifndef WINDOWS UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression&&) = default; UnaryBooleanFunctionExpression& operator=(UnaryBooleanFunctionExpression&&) = delete; -#endif virtual ~UnaryBooleanFunctionExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/UnaryExpression.h b/src/storm/storage/expressions/UnaryExpression.h index 05f84f6c2..77b6374a6 100644 --- a/src/storm/storage/expressions/UnaryExpression.h +++ b/src/storm/storage/expressions/UnaryExpression.h @@ -20,10 +20,8 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. UnaryExpression(UnaryExpression const& other) = default; UnaryExpression& operator=(UnaryExpression const& other) = delete; -#ifndef WINDOWS UnaryExpression(UnaryExpression&&) = default; UnaryExpression& operator=(UnaryExpression&&) = delete; -#endif virtual ~UnaryExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h index fe8fbaf45..134fa34eb 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.h @@ -26,10 +26,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& other) = default; UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression const& other) = delete; -#ifndef WINDOWS UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression&&) = default; UnaryNumericalFunctionExpression& operator=(UnaryNumericalFunctionExpression&&) = delete; -#endif + virtual ~UnaryNumericalFunctionExpression() = default; // Override base class methods. diff --git a/src/storm/storage/expressions/Variable.h b/src/storm/storage/expressions/Variable.h index f93a4dfd5..83ee9a13e 100644 --- a/src/storm/storage/expressions/Variable.h +++ b/src/storm/storage/expressions/Variable.h @@ -31,10 +31,9 @@ namespace storm { // Default-instantiate some copy/move construction/assignment. Variable(Variable const& other) = default; Variable& operator=(Variable const& other) = default; -#ifndef WINDOWS Variable(Variable&& other) = default; Variable& operator=(Variable&& other) = default; -#endif + /*! * Checks the two variables for equality. diff --git a/src/storm/storage/expressions/VariableExpression.h b/src/storm/storage/expressions/VariableExpression.h index 708ec35fc..f7d92ab52 100644 --- a/src/storm/storage/expressions/VariableExpression.h +++ b/src/storm/storage/expressions/VariableExpression.h @@ -20,10 +20,9 @@ namespace storm { // Instantiate constructors and assignments with their default implementations. VariableExpression(VariableExpression const&) = default; VariableExpression& operator=(VariableExpression const&) = delete; -#ifndef WINDOWS VariableExpression(VariableExpression&&) = default; VariableExpression& operator=(VariableExpression&&) = delete; -#endif + virtual ~VariableExpression() = default; // Override base class methods. diff --git a/src/storm/storage/prism/Assignment.h b/src/storm/storage/prism/Assignment.h index f53a8bf6a..43777a9d6 100644 --- a/src/storm/storage/prism/Assignment.h +++ b/src/storm/storage/prism/Assignment.h @@ -26,11 +26,9 @@ namespace storm { Assignment() = default; Assignment(Assignment const& other) = default; Assignment& operator=(Assignment const& other)= default; -#ifndef WINDOWS Assignment(Assignment&& other) = default; Assignment& operator=(Assignment&& other) = default; -#endif - + /*! * Retrieves the name of the variable that this assignment targets. * diff --git a/src/storm/storage/prism/BooleanVariable.h b/src/storm/storage/prism/BooleanVariable.h index 8431db46d..80b9ca51e 100644 --- a/src/storm/storage/prism/BooleanVariable.h +++ b/src/storm/storage/prism/BooleanVariable.h @@ -14,10 +14,8 @@ namespace storm { BooleanVariable() = default; BooleanVariable(BooleanVariable const& other) = default; BooleanVariable& operator=(BooleanVariable const& other)= default; -#ifndef WINDOWS BooleanVariable(BooleanVariable&& other) = default; BooleanVariable& operator=(BooleanVariable&& other) = default; -#endif /*! * Creates a boolean variable with the given constant initial value expression. diff --git a/src/storm/storage/prism/Command.h b/src/storm/storage/prism/Command.h index 31dc7a63a..983159c06 100644 --- a/src/storm/storage/prism/Command.h +++ b/src/storm/storage/prism/Command.h @@ -32,11 +32,9 @@ namespace storm { Command() = default; Command(Command const& other) = default; Command& operator=(Command const& other) = default; -#ifndef WINDOWS Command(Command&& other) = default; Command& operator=(Command&& other) = default; -#endif - + /*! * Retrieves the action name of this command. * diff --git a/src/storm/storage/prism/Constant.h b/src/storm/storage/prism/Constant.h index fad235e5c..dfa750eb5 100644 --- a/src/storm/storage/prism/Constant.h +++ b/src/storm/storage/prism/Constant.h @@ -35,11 +35,9 @@ namespace storm { Constant() = default; Constant(Constant const& other) = default; Constant& operator=(Constant const& other)= default; -#ifndef WINDOWS Constant(Constant&& other) = default; Constant& operator=(Constant&& other) = default; -#endif - + /*! * Retrieves the name of the constant. * diff --git a/src/storm/storage/prism/Formula.h b/src/storm/storage/prism/Formula.h index c1bb5aa67..17d2f0cbd 100644 --- a/src/storm/storage/prism/Formula.h +++ b/src/storm/storage/prism/Formula.h @@ -26,11 +26,9 @@ namespace storm { Formula() = default; Formula(Formula const& other) = default; Formula& operator=(Formula const& other)= default; -#ifndef WINDOWS Formula(Formula&& other) = default; Formula& operator=(Formula&& other) = default; -#endif - + /*! * Retrieves the name that is associated with this formula. * diff --git a/src/storm/storage/prism/InitialConstruct.h b/src/storm/storage/prism/InitialConstruct.h index a8aba856e..7eebe9428 100644 --- a/src/storm/storage/prism/InitialConstruct.h +++ b/src/storm/storage/prism/InitialConstruct.h @@ -32,11 +32,9 @@ namespace storm { InitialConstruct() = default; InitialConstruct(InitialConstruct const& other) = default; InitialConstruct& operator=(InitialConstruct const& other)= default; -#ifndef WINDOWS InitialConstruct(InitialConstruct&& other) = default; InitialConstruct& operator=(InitialConstruct&& other) = default; -#endif - + /*! * Retrieves the expression characterizing the initial states. * diff --git a/src/storm/storage/prism/IntegerVariable.h b/src/storm/storage/prism/IntegerVariable.h index d849167f2..3ddfd03e7 100644 --- a/src/storm/storage/prism/IntegerVariable.h +++ b/src/storm/storage/prism/IntegerVariable.h @@ -14,10 +14,8 @@ namespace storm { IntegerVariable() = default; IntegerVariable(IntegerVariable const& other) = default; IntegerVariable& operator=(IntegerVariable const& other)= default; -#ifndef WINDOWS IntegerVariable(IntegerVariable&& other) = default; IntegerVariable& operator=(IntegerVariable&& other) = default; -#endif /*! * Creates an integer variable with the given initial value expression. diff --git a/src/storm/storage/prism/Label.h b/src/storm/storage/prism/Label.h index 99690c583..eb07e7013 100644 --- a/src/storm/storage/prism/Label.h +++ b/src/storm/storage/prism/Label.h @@ -34,11 +34,9 @@ namespace storm { Label() = default; Label(Label const& other) = default; Label& operator=(Label const& other)= default; -#ifndef WINDOWS Label(Label&& other) = default; Label& operator=(Label&& other) = default; -#endif - + /*! * Retrieves the name that is associated with this label. * diff --git a/src/storm/storage/prism/LocatedInformation.h b/src/storm/storage/prism/LocatedInformation.h index c97a86a03..0204af130 100644 --- a/src/storm/storage/prism/LocatedInformation.h +++ b/src/storm/storage/prism/LocatedInformation.h @@ -22,11 +22,9 @@ namespace storm { LocatedInformation() = default; LocatedInformation(LocatedInformation const& other) = default; LocatedInformation& operator=(LocatedInformation const& other)= default; -#ifndef WINDOWS LocatedInformation(LocatedInformation&& other) = default; LocatedInformation& operator=(LocatedInformation&& other) = default; -#endif - + /*! * Retrieves the name of the file in which the information was found. * diff --git a/src/storm/storage/prism/Module.h b/src/storm/storage/prism/Module.h index 7b26ed2da..9c1286805 100644 --- a/src/storm/storage/prism/Module.h +++ b/src/storm/storage/prism/Module.h @@ -48,11 +48,9 @@ namespace storm { Module() = default; Module(Module const& other) = default; Module& operator=(Module const& other)= default; -#ifndef WINDOWS Module(Module&& other) = default; Module& operator=(Module&& other) = default; -#endif - + /*! * Retrieves the number of boolean variables in the module. * diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index ccf56ead6..4fe0f8432 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -63,11 +63,9 @@ namespace storm { Program() = default; Program(Program const& other) = default; Program& operator=(Program const& other) = default; -#ifndef WINDOWS Program(Program&& other) = default; Program& operator=(Program&& other) = default; -#endif - + /*! * Retrieves the model type of the model. * diff --git a/src/storm/storage/prism/RewardModel.h b/src/storm/storage/prism/RewardModel.h index 1fee6c901..cda14bdc4 100644 --- a/src/storm/storage/prism/RewardModel.h +++ b/src/storm/storage/prism/RewardModel.h @@ -31,11 +31,9 @@ namespace storm { RewardModel() = default; RewardModel(RewardModel const& other) = default; RewardModel& operator=(RewardModel const& other)= default; -#ifndef WINDOWS RewardModel(RewardModel&& other) = default; RewardModel& operator=(RewardModel&& other) = default; -#endif - + /*! * Retrieves the name of the reward model. * diff --git a/src/storm/storage/prism/StateActionReward.h b/src/storm/storage/prism/StateActionReward.h index 8e56a8829..d54d99b88 100644 --- a/src/storm/storage/prism/StateActionReward.h +++ b/src/storm/storage/prism/StateActionReward.h @@ -38,11 +38,9 @@ namespace storm { StateActionReward() = default; StateActionReward(StateActionReward const& other) = default; StateActionReward& operator=(StateActionReward const& other)= default; -#ifndef WINDOWS StateActionReward(StateActionReward&& other) = default; StateActionReward& operator=(StateActionReward&& other) = default; -#endif - + /*! * Retrieves the action name that is associated with this transition reward. * diff --git a/src/storm/storage/prism/StateReward.h b/src/storm/storage/prism/StateReward.h index 562a0a5bc..b7075588c 100644 --- a/src/storm/storage/prism/StateReward.h +++ b/src/storm/storage/prism/StateReward.h @@ -35,11 +35,9 @@ namespace storm { StateReward() = default; StateReward(StateReward const& other) = default; StateReward& operator=(StateReward const& other)= default; -#ifndef WINDOWS StateReward(StateReward&& other) = default; StateReward& operator=(StateReward&& other) = default; -#endif - + /*! * Retrieves the state predicate that is associated with this state reward. * diff --git a/src/storm/storage/prism/SystemCompositionConstruct.h b/src/storm/storage/prism/SystemCompositionConstruct.h index 0eb016487..d4f1aeba1 100644 --- a/src/storm/storage/prism/SystemCompositionConstruct.h +++ b/src/storm/storage/prism/SystemCompositionConstruct.h @@ -26,11 +26,9 @@ namespace storm { SystemCompositionConstruct() = default; SystemCompositionConstruct(SystemCompositionConstruct const& other) = default; SystemCompositionConstruct& operator=(SystemCompositionConstruct const& other)= default; -#ifndef WINDOWS SystemCompositionConstruct(SystemCompositionConstruct&& other) = default; SystemCompositionConstruct& operator=(SystemCompositionConstruct&& other) = default; -#endif - + Composition const& getSystemComposition() const; friend std::ostream& operator<<(std::ostream& stream, SystemCompositionConstruct const& systemCompositionConstruct); diff --git a/src/storm/storage/prism/TransitionReward.h b/src/storm/storage/prism/TransitionReward.h index 64f0bd903..5f4f9e19d 100644 --- a/src/storm/storage/prism/TransitionReward.h +++ b/src/storm/storage/prism/TransitionReward.h @@ -41,11 +41,9 @@ namespace storm { TransitionReward() = default; TransitionReward(TransitionReward const& other) = default; TransitionReward& operator=(TransitionReward const& other)= default; -#ifndef WINDOWS TransitionReward(TransitionReward&& other) = default; TransitionReward& operator=(TransitionReward&& other) = default; -#endif - + /*! * Retrieves the action name that is associated with this transition reward. * diff --git a/src/storm/storage/prism/Update.h b/src/storm/storage/prism/Update.h index f4f4b8384..b27ddfff4 100644 --- a/src/storm/storage/prism/Update.h +++ b/src/storm/storage/prism/Update.h @@ -26,11 +26,9 @@ namespace storm { Update() = default; Update(Update const& other) = default; Update& operator=(Update const& other)= default; -#ifndef WINDOWS Update(Update&& other) = default; Update& operator=(Update&& other) = default; -#endif - + /*! * Retrieves the expression for the likelihood of this update. * diff --git a/src/storm/storage/prism/Variable.h b/src/storm/storage/prism/Variable.h index 3d379cd25..42ba9aec0 100644 --- a/src/storm/storage/prism/Variable.h +++ b/src/storm/storage/prism/Variable.h @@ -15,11 +15,9 @@ namespace storm { // Create default implementations of constructors/assignment. Variable(Variable const& otherVariable) = default; Variable& operator=(Variable const& otherVariable)= default; -#ifndef WINDOWS Variable(Variable&& otherVariable) = default; Variable& operator=(Variable&& otherVariable) = default; -#endif - + /*! * Retrieves the name of the variable. * From 697ae21b6f9e2993772ec4c16e2e83ddf2ad8dfd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 25 Apr 2017 15:44:17 +0200 Subject: [PATCH 3/7] Suppress warning --- src/storm/storage/jani/JSONExporter.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index bfddea091..65cab6fb1 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -525,6 +525,7 @@ namespace storm { } } STORM_LOG_ASSERT(false, "Expression variable '" << expression.getVariableName() << "' not known in Jani data structures."); + return modernjson::json(); // should not reach this point. } boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) { modernjson::json opDecl; From 6c8d2a31fcdd6c6795e16fe2aa3c528888cc7439 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 25 Apr 2017 16:10:32 +0200 Subject: [PATCH 4/7] Better error messages when something is wrong with the argument given. --- src/storm/settings/Argument.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/storm/settings/Argument.cpp b/src/storm/settings/Argument.cpp index 7ebc3d484..ddb39c0ab 100644 --- a/src/storm/settings/Argument.cpp +++ b/src/storm/settings/Argument.cpp @@ -68,9 +68,9 @@ namespace storm { template void Argument::setFromDefaultValue() { - STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument has none."); + STORM_LOG_THROW(this->hasDefaultValue, storm::exceptions::IllegalFunctionCallException, "Unable to set value from default value, because the argument " << name << " has none."); bool result = this->setFromTypeValue(this->defaultValue, false); - STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument, because it was rejected."); + STORM_LOG_THROW(result, storm::exceptions::IllegalArgumentValueException, "Unable to assign default value to argument " << name << ", because it was rejected."); } template @@ -95,7 +95,7 @@ namespace storm { switch (this->argumentType) { case ArgumentType::Integer: return inferToInteger(ArgumentType::Integer, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as integer."); break; + default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as integer."); break; } } @@ -105,7 +105,7 @@ namespace storm { switch (this->argumentType) { case ArgumentType::UnsignedInteger: return inferToUnsignedInteger(ArgumentType::UnsignedInteger, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as unsigned integer."); break; + default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as unsigned integer."); break; } } @@ -115,7 +115,7 @@ namespace storm { switch (this->argumentType) { case ArgumentType::Double: return inferToDouble(ArgumentType::Double, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as double."); break; + default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as double."); break; } } @@ -124,7 +124,7 @@ namespace storm { switch (this->argumentType) { case ArgumentType::Boolean: return inferToBoolean(ArgumentType::Boolean, this->getArgumentValue()); - default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value as boolean."); break; + default: STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve argument value for " << name << " as Boolean."); break; } } From 291f5ecd47d1c1efcc284fdbd22fd3808e4793ce Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 25 Apr 2017 16:26:15 +0200 Subject: [PATCH 5/7] First version of Jani-to-Dot. --- src/storm/cli/cli.cpp | 8 ++++++ src/storm/settings/modules/IOSettings.cpp | 19 ++++++++++++++ src/storm/settings/modules/IOSettings.h | 22 ++++++++++++++++ src/storm/storage/jani/Automaton.cpp | 31 +++++++++++++++++++++++ src/storm/storage/jani/Automaton.h | 2 ++ src/storm/storage/jani/Model.cpp | 11 ++++++++ src/storm/storage/jani/Model.h | 2 ++ 7 files changed, 95 insertions(+) diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index bdba45a30..7310f56c6 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -15,6 +15,7 @@ #include "storm/settings/modules/JaniExportSettings.h" #include "storm/utility/resources.h" +#include "storm/utility/file.h" #include "storm/utility/storm-version.h" @@ -241,6 +242,13 @@ namespace storm { properties.push_back(input.second.at(propName)); } } + + if(ioSettings.isExportJaniDotSet()) { + std::ofstream out; + storm::utility::openFile(ioSettings.getExportJaniDotFilename(), out); + model.asJaniModel().writeDotToStream(out); + storm::utility::closeFile(out); + } } diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index 1ade861dd..51d7fe512 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/src/storm/settings/modules/IOSettings.cpp @@ -19,6 +19,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; + const std::string IOSettings::exportJaniDotOptionName = "exportjanidot"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::explicitDrnOptionName = "explicit-drn"; @@ -40,6 +41,7 @@ namespace storm { const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; const std::string IOSettings::noBuildOptionName = "nobuild"; const std::string IOSettings::fullModelBuildOptionName = "buildfull"; + const std::string IOSettings::buildChoiceLabelOptionName = "buildchoicelab"; const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; const std::string IOSettings::propertyOptionName = "prop"; @@ -50,6 +52,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, "", "If given, the loaded jani model will be written to the specified file in the dot format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) @@ -65,6 +69,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, include choice labels").build()); this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build()) @@ -94,6 +99,14 @@ namespace storm { std::string IOSettings::getExportDotFilename() const { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isExportJaniDotSet() const { + return this->getOption(exportJaniDotOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportJaniDotFilename() const { + return this->getOption(exportJaniDotOptionName).getArgumentByName("filename").getValueAsString(); + } bool IOSettings::isExportExplicitSet() const { return this->getOption(exportExplicitOptionName).getHasOptionBeenSet(); @@ -225,6 +238,10 @@ namespace storm { return this->getOption(noBuildOptionName).getHasOptionBeenSet(); } + bool IOSettings::isBuildChoiceLabelsSet() const { + return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); + } + bool IOSettings::isPropertySet() const { return this->getOption(propertyOptionName).getHasOptionBeenSet(); } @@ -247,6 +264,8 @@ namespace storm { // Ensure that not two explicit input models were given. STORM_LOG_THROW(!isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "Explicit model "); + STORM_LOG_THROW(!isExportJaniDotSet() || isJaniInputSet(), storm::exceptions::InvalidSettingsException, "Jani-to-dot export is only available for jani models" ); + // Ensure that the model was given either symbolically or explicitly. STORM_LOG_THROW(!isJaniInputSet() || !isPrismInputSet() || !isExplicitSet() || !isExplicitDRNSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both."); diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h index 0e329b840..d7674e9f2 100644 --- a/src/storm/settings/modules/IOSettings.h +++ b/src/storm/settings/modules/IOSettings.h @@ -35,6 +35,20 @@ namespace storm { */ std::string getExportDotFilename() const; + /*! + * Retrieves whether the export-to-dot option for jani was set. + * + * @return True if the export-to-jani-dot option was set. + */ + bool isExportJaniDotSet() const; + + /*! + * Retrieves the name in which to write the jani model in dot format, if the export-to-jani-dot option was set. + * + * @return The name of the file in which to write the exported model. + */ + std::string getExportJaniDotFilename() const; + /*! * Retrieves whether the export-to-explicit option was set * @@ -277,6 +291,12 @@ namespace storm { */ bool isBuildFullModelSet() const; + /*! + * Retrieves whether the choice labels should be build + * @return + */ + bool isBuildChoiceLabelsSet() const; + bool check() const override; void finalize() override; @@ -286,6 +306,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string exportDotOptionName; + static const std::string exportJaniDotOptionName; static const std::string exportExplicitOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; @@ -308,6 +329,7 @@ namespace storm { static const std::string prismCompatibilityOptionShortName; static const std::string fullModelBuildOptionName; static const std::string noBuildOptionName; + static const std::string buildChoiceLabelOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; static const std::string propertyOptionName; diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 88641c318..00e5bf14b 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -528,5 +528,36 @@ namespace storm { return result; } + + void Automaton::writeDotToStream(std::ostream& outStream) const { + outStream << "\tsubgraph " << name << " {" << std::endl; + + // Write all locations to the stream. + uint64_t locIndex = 0; + for (auto const& loc : locations) { + outStream << "\t" << name << "_s" << locIndex << "[ label=\"" << loc.getName() << "\"];" << std::endl; + ++locIndex; + } + // Write for each edge an node to the stream; + uint64_t edgeIndex = 0; + for (auto const& edge : edges) { + outStream << "\t" << name << "_e" << edgeIndex << ";" << std::endl; + ++edgeIndex; + } + + // Connect edges + edgeIndex = 0; + for (auto const& edge : edges) { + outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << ";" << std::endl; + for (auto const& edgeDest : edge.getDestinations()) { + outStream << "\t" << name << "_e" << edgeIndex << " -> " << name << "_s" << edgeDest.getLocationIndex() << ";" << std::endl; + } + ++edgeIndex; + } + + + outStream << "\t}" << std::endl; + + } } } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 6c940d464..cf8c92fd7 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -371,6 +371,8 @@ namespace storm { * Checks the automaton for linearity. */ bool isLinear() const; + + void writeDotToStream(std::ostream& outStream = std::cout) const; private: /// The name of the automaton. diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index e7ea47349..7cd420a65 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1165,5 +1165,16 @@ namespace storm { return newModel; } + + void Model::writeDotToStream(std::ostream& outStream) const { + outStream << "digraph " << name << " {" << std::endl; + + for (auto const& automaton : automata) { + automaton.writeDotToStream(outStream); + outStream << std::endl; + } + + outStream << "}"; + } } } diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 201e1ecc5..bb0b48f26 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -448,6 +448,8 @@ namespace storm { * @return */ bool reusesActionsInComposition() const; + + void writeDotToStream(std::ostream& outStream = std::cout) const; /// The name of the silent action. static const std::string SILENT_ACTION_NAME; From 6a3310f7eead9e9ba9e3b6fd4882728af470cf4a Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 25 Apr 2017 18:15:33 +0200 Subject: [PATCH 6/7] Improved Jani-to-dot: - Fixed problems when the model name contained a dot - Edges are displayed nicer - Action names are displayed. --- src/storm/storage/jani/Automaton.cpp | 6 +++--- src/storm/storage/jani/Automaton.h | 2 +- src/storm/storage/jani/Model.cpp | 22 ++++++++++++++++++++-- 3 files changed, 24 insertions(+), 6 deletions(-) diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 00e5bf14b..e3ec908c1 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -529,7 +529,7 @@ namespace storm { return result; } - void Automaton::writeDotToStream(std::ostream& outStream) const { + void Automaton::writeDotToStream(std::ostream& outStream, std::vector const& actionNames) const { outStream << "\tsubgraph " << name << " {" << std::endl; // Write all locations to the stream. @@ -541,14 +541,14 @@ namespace storm { // Write for each edge an node to the stream; uint64_t edgeIndex = 0; for (auto const& edge : edges) { - outStream << "\t" << name << "_e" << edgeIndex << ";" << std::endl; + outStream << "\t" << name << "_e" << edgeIndex << "[ label=\"\" , shape=circle, width=.2, style=filled, fillcolor=\"black\"];" << std::endl; ++edgeIndex; } // Connect edges edgeIndex = 0; for (auto const& edge : edges) { - outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << ";" << std::endl; + outStream << "\t" << name << "_s" << edge.getSourceLocationIndex() << " -> " << name << "_e" << edgeIndex << " [label=\"" << actionNames.at(edge.getActionIndex()) << "\"];" << std::endl; for (auto const& edgeDest : edge.getDestinations()) { outStream << "\t" << name << "_e" << edgeIndex << " -> " << name << "_s" << edgeDest.getLocationIndex() << ";" << std::endl; } diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index cf8c92fd7..37b4e9755 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -372,7 +372,7 @@ namespace storm { */ bool isLinear() const; - void writeDotToStream(std::ostream& outStream = std::cout) const; + void writeDotToStream(std::ostream& outStream, std::vector const& actionNames) const; private: /// The name of the automaton. diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 7cd420a65..27232786b 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1,5 +1,7 @@ #include "storm/storage/jani/Model.h" +#include + #include "storm/storage/expressions/ExpressionManager.h" @@ -1166,11 +1168,27 @@ namespace storm { return newModel; } + + // Helper for writeDotToStream: + + std::string filterName(std::string const& text) { + std::string result = text; + std::replace_if(result.begin() , result.end() , + [] (const char& c) { return std::ispunct(c) ;},'_'); + return result; + } + + void Model::writeDotToStream(std::ostream& outStream) const { - outStream << "digraph " << name << " {" << std::endl; + outStream << "digraph " << filterName(name) << " {" << std::endl; + + std::vector actionNames; + for (auto const& act : actions) { + actionNames.push_back(act.getName()); + } for (auto const& automaton : automata) { - automaton.writeDotToStream(outStream); + automaton.writeDotToStream(outStream, actionNames); outStream << std::endl; } From 524efc616d71713a35c4fcf3edcb50d1b6bc4170 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 25 Apr 2017 19:45:26 +0200 Subject: [PATCH 7/7] Jit-builder now gives better diagnostics when nofixdl option is set. --- .../builder/jit/ExplicitJitJaniModelBuilder.cpp | 15 +++++++++++++-- src/storm/builder/jit/ModelComponentsBuilder.cpp | 3 ++- 2 files changed, 15 insertions(+), 3 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 6df0210e9..96c2738ed 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -32,6 +32,9 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/JitBuilderSettings.h" +#include "storm/settings/modules/CoreSettings.h" + + #include "storm/utility/OsDetection.h" #include "storm-config.h" @@ -535,6 +538,8 @@ namespace storm { } modelData["double"] = cpptempl::make_data(list); + modelData["dontFixDeadlocks"] = storm::settings::getModule().isDontFixDeadlocksSet(); + // If we are building a possibly parametric model, we need to create the parameters. if (std::is_same::value) { generateParameters(modelData); @@ -1657,7 +1662,6 @@ namespace storm { #include "storm/builder/RewardModelInformation.h" #include "storm/utility/constants.h" - #include "storm/exceptions/WrongFormatException.h" namespace storm { @@ -2278,7 +2282,14 @@ namespace storm { // Explore all edges that participate in synchronization vectors. exploreSynchronizingEdges(currentState, behaviour, statesToExplore); } - + + {% if dontFixDeadlocks %} + if (behaviour.empty() && behaviour.isExpanded() ) { + std::cout << currentState << std::endl; + throw storm::exceptions::WrongFormatException("Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled."); + } + {% endif %} + this->addStateBehaviour(currentIndex, behaviour); behaviour.clear(); } diff --git a/src/storm/builder/jit/ModelComponentsBuilder.cpp b/src/storm/builder/jit/ModelComponentsBuilder.cpp index 6f61feb19..752ab9b31 100644 --- a/src/storm/builder/jit/ModelComponentsBuilder.cpp +++ b/src/storm/builder/jit/ModelComponentsBuilder.cpp @@ -81,7 +81,8 @@ namespace storm { } } else { if (behaviour.isExpanded() && dontFixDeadlocks) { - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled."); + // Skip on purpose; Error is produced in the generated code to provide better diagnostics. + //STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled."); } else { // Add the self-loop in the transition matrix. transitionMatrixBuilder->addNextValue(currentRow, currentRowGroup, storm::utility::one());