few fixes to jani game-based abstraction

src/storm/abstraction/jani/EdgeAbstractor.cpp

@@ -639,7 +639,13 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             BottomStateResult<DdType> EdgeAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables, boost::optional<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& locationVariables) {
                 // Compute the reachable states that have this edge enabled.
-                storm::dd::Bdd<DdType> reachableStatesWithEdge = (reachableStates && abstractGuard && this->getAbstractionInformation().encodeLocation(locationVariables.get().first, edge.get().getSourceLocationIndex())).existsAbstract(this->getAbstractionInformation().getSourceLocationVariables());
+                storm::dd::Bdd<DdType> 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<DdType> 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);
+                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()) {

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -38,7 +38,7 @@ namespace storm {
             JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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.

src/storm/adapters/MathsatExpressionAdapter.h

@@ -273,6 +273,8 @@ namespace storm {
 					} else if (msat_is_rational_type(env, msat_term_get_type(term))) {
                         return manager.rational(storm::utility::convertNumber<storm::RationalNumber>(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.

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<uint_fast64_t> const& edgeIndices) {

src/storm/storage/jani/Model.cpp

@@ -462,9 +462,13 @@ namespace storm {
             // Assert the values of the constants.
             for (auto const& constant : this->getConstants()) {
                 if (constant.isDefined()) {
+                    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.
             for (auto const& variable : newAutomaton.getVariables().getBoundedIntegerVariables()) {
                 solver->add(variable.getExpressionVariable() >= variable.getLowerBound());

src/storm/storage/prism/Program.cpp

@@ -1381,9 +1381,13 @@ namespace storm {
             // Assert the values of the constants.
             for (auto const& constant : this->getConstants()) {
                 if (constant.isDefined()) {
+                    if (constant.getType().isBooleanType()) {
+                        solver->add(storm::expressions::iff(constant.getExpressionVariable(),constant.getExpression()));
+                    } else {
                         solver->add(constant.getExpressionVariable() == constant.getExpression());
                     }
                 }
+            }
             
             // Assert the bounds of the global variables.
             for (auto const& variable : this->getGlobalIntegerVariables()) {