From d66047e3b76ac457604231575437301535bd1835 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 14 May 2018 07:59:21 +0200 Subject: [PATCH] few fixes to jani game-based abstraction --- src/storm/abstraction/jani/EdgeAbstractor.cpp | 14 ++++++++++++-- .../abstraction/jani/JaniMenuGameAbstractor.cpp | 2 +- src/storm/adapters/MathsatExpressionAdapter.h | 4 +++- src/storm/storage/jani/Automaton.cpp | 4 ++-- src/storm/storage/jani/Model.cpp | 6 +++++- src/storm/storage/prism/Program.cpp | 6 +++++- 6 files changed, 28 insertions(+), 8 deletions(-) diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index a1fbe6fe9..ebd7b5839 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -639,7 +639,13 @@ namespace storm { template BottomStateResult EdgeAbstractor::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables, boost::optional> const& locationVariables) { // Compute the reachable states that have this edge enabled. - storm::dd::Bdd reachableStatesWithEdge = (reachableStates && abstractGuard && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex())).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); + storm::dd::Bdd reachableStatesWithEdge; + if (locationVariables) { + reachableStatesWithEdge = (reachableStates && abstractGuard && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex())).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); + } else { + reachableStatesWithEdge = (reachableStates && abstractGuard).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables()); + } + STORM_LOG_TRACE("Computing bottom state transitions of edge with guard " << edge.get().getGuard()); BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); @@ -653,7 +659,11 @@ namespace storm { // Use the state abstractor to compute the set of abstract states that has this edge enabled but still // has a transition to a bottom state. bottomStateAbstractor.constrain(reachableStatesWithEdge); - result.states = bottomStateAbstractor.getAbstractStates() && reachableStatesWithEdge && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex()); + if (locationVariables) { + result.states = bottomStateAbstractor.getAbstractStates() && reachableStatesWithEdge && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex()); + } else { + result.states = bottomStateAbstractor.getAbstractStates() && reachableStatesWithEdge; + } // If the result is empty one time, we can skip the bottom state computation from now on. if (result.states.isZero()) { diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index b41ccf418..4b30c61bd 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -38,7 +38,7 @@ namespace storm { JaniMenuGameAbstractor::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) { // Check whether the model is linear as the abstraction requires this. - STORM_LOG_THROW(model.isLinear(), storm::exceptions::WrongFormatException, "Cannot create abstract model from non-linear model."); + STORM_LOG_WARN_COND(model.isLinear(), "The model appears to contain non-linear expressions, which may cause malfunctioning of the abstraction."); // For now, we assume that there is a single module. If the program has more than one module, it needs // to be flattened before the procedure. diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index 4b4d7cb57..0b111a10f 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -273,7 +273,9 @@ namespace storm { } else if (msat_is_rational_type(env, msat_term_get_type(term))) { return manager.rational(storm::utility::convertNumber(termString)); } - } + } else if (msat_term_is_term_ite(env, term)) { + return storm::expressions::ite(translateExpression(msat_term_get_arg(term, 0)), translateExpression(msat_term_get_arg(term, 1)), translateExpression(msat_term_get_arg(term, 2))); + } // If all other cases did not apply, we cannot represent the term in our expression framework. char* termAsCString = msat_term_repr(term); diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index f4c65c759..7d856e56c 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -452,9 +452,9 @@ namespace storm { result &= location.isLinear(); } if (result) { - return edges.isLinear(); + result &= edges.isLinear(); } - return false; + return result; } void Automaton::restrictToEdges(boost::container::flat_set const& edgeIndices) { diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 47533126c..a6491a884 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -462,7 +462,11 @@ namespace storm { // Assert the values of the constants. for (auto const& constant : this->getConstants()) { if (constant.isDefined()) { - solver->add(constant.getExpressionVariable() == constant.getExpression()); + if (constant.isBooleanConstant()) { + solver->add(storm::expressions::iff(constant.getExpressionVariable(), constant.getExpression())); + } else { + solver->add(constant.getExpressionVariable() == constant.getExpression()); + } } } // Assert the bounds of the global variables. diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 228df8541..cda98bc09 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1381,7 +1381,11 @@ namespace storm { // Assert the values of the constants. for (auto const& constant : this->getConstants()) { if (constant.isDefined()) { - solver->add(constant.getExpressionVariable() == constant.getExpression()); + if (constant.getType().isBooleanType()) { + solver->add(storm::expressions::iff(constant.getExpressionVariable(),constant.getExpression())); + } else { + solver->add(constant.getExpressionVariable() == constant.getExpression()); + } } }