From 905f6fc970b3cfd6b26ab94be049184376a00cba Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Wed, 22 Aug 2018 09:17:31 +0200 Subject: [PATCH] Create lattice from model and formulas --- src/storm-pars-cli/storm-pars.cpp | 43 +++++-------------------------- src/storm-pars/analysis/Lattice.h | 39 +++++++++++++++++++++++++--- 2 files changed, 42 insertions(+), 40 deletions(-) diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index b7da6c37e..7bf13cc18 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -461,7 +461,7 @@ namespace storm { if (parSettings.isMonotonicityAnalysisSet()) { std::cout << "Hello, Jip1" << std::endl; -// STORM_LOG_THROW(storm::settings::getModule().isBisimulationSet(), storm::exceptions::InvalidSettingsException, "Monotonicity analysis requires bisimulation"); + // Simplify the model storm::utility::Stopwatch simplifyingWatch(true); if (model->isOfType(storm::models::ModelType::Dtmc)) { auto consideredModel = (model->as>()); @@ -486,7 +486,7 @@ namespace storm { } model = simplifier.getSimplifiedModel(); } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type."); + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform monotonicity analysis on the provided model type."); } simplifyingWatch.stop(); @@ -508,35 +508,10 @@ namespace storm { storm::utility::Stopwatch latticeWatch(true); std::vector> 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() - || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula"); - std::shared_ptr> sparseModel = model->as>(); - storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*sparseModel); - - storm::storage::BitVector phiStates; - storm::storage::BitVector psiStates; - if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { - phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - } else { - phiStates = storm::storage::BitVector(sparseModel.get()->getNumberOfStates(), true); - psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - } - - // Get the maybeStates - std::pair statesWithProbability01 = storm::utility::graph::performProb01(sparseModel.get()->getBackwardTransitions(), phiStates, psiStates); - storm::storage::BitVector topStates = statesWithProbability01.second; - storm::storage::BitVector bottomStates = statesWithProbability01.first; - STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states"); - STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states"); // Transform to Lattice - storm::storage::SparseMatrix matrix = sparseModel.get()->getTransitionMatrix(); - storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice(matrix, topStates, bottomStates); + storm::analysis::Lattice* lattice = storm::analysis::Lattice::toLattice(sparseModel, formulas); latticeWatch.stop(); STORM_PRINT(std::endl << "Time for lattice creation: " << latticeWatch << "." << std::endl << std::endl); @@ -561,7 +536,7 @@ namespace storm { } - + storm::storage::SparseMatrix matrix = sparseModel.get()->getTransitionMatrix(); for (uint_fast64_t i = 0; i < sparseModel.get()->getNumberOfStates(); ++i) { // go over all rows auto row = matrix.getRow(i); @@ -618,13 +593,11 @@ namespace storm { } myfile << "\tsubgraph legend {" << std::endl; -// myfile << "\t\trank=\"source\";" << std::endl; myfile << "\t\tnode [color=white];" << std::endl; myfile << "\t\tedge [style=invis];" << std::endl; - myfile << "\t\tedge [style=invis];" << std::endl; - myfile << "\t\tt0 [label=\"incr+decr false\", fontcolor=red];" << std::endl; - myfile << "\t\tt1 [label=\"incr false (dashed)\", fontcolor=blue];" << std::endl; - myfile << "\t\tt2 [label=\"decr false (dotted)\", fontcolor=blue];" << std::endl; + myfile << "\t\tt0 [label=\"incr? and decr?\", fontcolor=red];" << std::endl; + myfile << "\t\tt1 [label=\"incr? (dashed)\", fontcolor=blue];" << std::endl; + myfile << "\t\tt2 [label=\"decr? (dotted)\", fontcolor=blue];" << std::endl; myfile << "\t}" << std::endl; myfile << "}" << std::endl; @@ -648,8 +621,6 @@ namespace storm { return; } - - std::vector> regions = parseRegions(model); std::string samplesAsString = parSettings.getSamples(); SampleInformation samples; diff --git a/src/storm-pars/analysis/Lattice.h b/src/storm-pars/analysis/Lattice.h index 34242fe75..8248b74d9 100644 --- a/src/storm-pars/analysis/Lattice.h +++ b/src/storm-pars/analysis/Lattice.h @@ -7,10 +7,16 @@ #include #include +#include +#include #include "storm/models/sparse/Model.h" #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" +#include "storm/utility/macros.h" +#include "storm/utility/graph.h" +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/NotSupportedException.h" namespace storm { @@ -94,10 +100,35 @@ namespace storm { * @return pointer to the created Lattice. */ template - static Lattice* toLattice(storm::storage::SparseMatrix matrix, - storm::storage::BitVector topStates, - storm::storage::BitVector bottomStates) { - uint_fast64_t numberOfStates = matrix.getColumnCount(); + static Lattice* toLattice(std::shared_ptr> sparseModel, std::vector> formulas) { + 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() + || (*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()), storm::exceptions::NotSupportedException, "Expecting until formula"); + + uint_fast64_t numberOfStates = sparseModel.get()->getNumberOfStates(); + + storm::modelchecker::SparsePropositionalModelChecker> propositionalChecker(*sparseModel); + storm::storage::BitVector phiStates; + storm::storage::BitVector psiStates; + if ((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().isUntilFormula()) { + phiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } else { + phiStates = storm::storage::BitVector(numberOfStates, true); + psiStates = propositionalChecker.check((*(formulas[0])).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } + + // Get the maybeStates + std::pair statesWithProbability01 = storm::utility::graph::performProb01(sparseModel.get()->getBackwardTransitions(), phiStates, psiStates); + storm::storage::BitVector topStates = statesWithProbability01.second; + storm::storage::BitVector bottomStates = statesWithProbability01.first; + + STORM_LOG_THROW(topStates.begin() != topStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no 1 states"); + STORM_LOG_THROW(bottomStates.begin() != bottomStates.end(), storm::exceptions::NotImplementedException, "Formula yields to no zero states"); + + // Transform to Lattice + auto matrix = sparseModel.get()->getTransitionMatrix(); // Transform the transition matrix into a vector containing the states with the state to which the transition goes. std::vector stateVector = std::vector({});