Add check on amount of formulas, fix typo

src/storm-pars-cli/storm-pars.cpp

@@ -507,11 +507,14 @@ namespace storm {
                 std::cout << "Hello, Jip2" << std::endl;
                 storm::utility::Stopwatch latticeWatch(true);
 
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
                 std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(input.properties);
 
+                STORM_LOG_THROW((++formulas.begin()) == formulas.end(), storm::exceptions::NotSupportedException, "Only one formula allowed for monotonicity analysis");
                 STORM_LOG_THROW((*(formulas[0])).isProbabilityOperatorFormula() && (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula(), storm::exceptions::NotSupportedException, "Expecting until formula");
+
+                std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->as<storm::models::sparse::Model<ValueType>>();
                 storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<ValueType>> propositionalChecker(*sparseModel);
+
                 storm::storage::BitVector phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector();
                 storm::storage::BitVector psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); //right
 
@@ -520,7 +523,7 @@ namespace storm {
                 storm::storage::BitVector topStates = statesWithProbability01.second;
                 storm::storage::BitVector bottomStates = statesWithProbability01.first;
 
-                // Transform to LatticeLattice
+                // Transform to Lattice
                 storm::storage::SparseMatrix<ValueType> matrix = sparseModel.get()->getTransitionMatrix();
                 storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice<ValueType>(matrix, topStates, bottomStates);
 

src/storm-pars/analysis/Lattice.h

@@ -133,7 +133,6 @@ namespace storm {
                                     && seenStates[currentState->successor1]
                                     && seenStates[currentState->successor2]) {
 
-
                                     // Otherwise, check how the two states compare, and add if the comparison is possible.
                                     uint_fast64_t successor1 = currentState->successor1;
                                     uint_fast64_t successor2 = currentState->successor2;