sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

started polishing pstorm a bit 

Former-commit-id: bd9c2a42a7
tempestpy_adaptions
dehnert 10 years ago
parent
d63086d7e3
commit
3f44b1295f
2 changed files with 51 additions and 335 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 378
      src/stormParametric.cpp
  2. 8
      src/utility/cli.h

378
src/stormParametric.cpp
View File

@ -17,112 +17,6 @@
#include "src/storage/parameters.h" #include "src/storage/parameters.h"
#include "src/models/Dtmc.h" #include "src/models/Dtmc.h"
//std::tuple<storm::RationalFunction, boost::optional<storm::storage::SparseMatrix<storm::RationalFunction>>, boost::optional<std::vector<storm::RationalFunction>>, boost::optional<storm::storage::BitVector>, boost::optional<double>, boost::optional<bool>> computeReachabilityProbability(storm::models::Dtmc<storm::RationalFunction> const& dtmc, std::shared_ptr<storm::properties::prctl::PrctlFilter<double>> const& filterFormula) {
// // The first thing we need to do is to make sure the formula is of the correct form and - if so - extract
// // the bitvector representation of the atomic propositions.
//
// std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> stateFormula = std::dynamic_pointer_cast<storm::properties::prctl::AbstractStateFormula<double>>(filterFormula->getChild());
// std::shared_ptr<storm::properties::prctl::AbstractPathFormula<double>> pathFormula;
// boost::optional<double> threshold;
// boost::optional<bool> strict;
// if (stateFormula != nullptr) {
// std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<double>> probabilisticBoundFormula = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<double>>(stateFormula);
// STORM_LOG_THROW(probabilisticBoundFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted.");
// STORM_LOG_THROW(probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS_EQUAL || probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties with upper probability bounds are permitted.");
//
// threshold = probabilisticBoundFormula->getBound();
// strict = probabilisticBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS;
// pathFormula = probabilisticBoundFormula->getChild();
// } else {
// pathFormula = std::dynamic_pointer_cast<storm::properties::prctl::AbstractPathFormula<double>>(filterFormula->getChild());
// }
//
// STORM_LOG_THROW(pathFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted.");
//
// std::shared_ptr<storm::properties::prctl::Until<double>> untilFormula = std::dynamic_pointer_cast<storm::properties::prctl::Until<double>>(pathFormula);
// std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> phiStateFormula;
// std::shared_ptr<storm::properties::prctl::AbstractStateFormula<double>> psiStateFormula;
// if (untilFormula != nullptr) {
// phiStateFormula = untilFormula->getLeft();
// psiStateFormula = untilFormula->getRight();
// } else {
// std::shared_ptr<storm::properties::prctl::Eventually<double>> eventuallyFormula = std::dynamic_pointer_cast<storm::properties::prctl::Eventually<double>>(pathFormula);
// STORM_LOG_THROW(eventuallyFormula != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *filterFormula << " for parametric model checking. Note that only unbounded reachability properties are permitted.");
// phiStateFormula = std::shared_ptr<storm::properties::prctl::Ap<double>>(new storm::properties::prctl::Ap<double>("true"));
// psiStateFormula = eventuallyFormula->getChild();
// }
//
// // Now we need to make sure the formulas defining the phi and psi states are just labels.
// std::shared_ptr<storm::properties::prctl::Ap<double>> phiStateFormulaApFormula = std::dynamic_pointer_cast<storm::properties::prctl::Ap<double>>(phiStateFormula);
// std::shared_ptr<storm::properties::prctl::Ap<double>> psiStateFormulaApFormula = std::dynamic_pointer_cast<storm::properties::prctl::Ap<double>>(psiStateFormula);
// STORM_LOG_THROW(phiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *phiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position.");
// STORM_LOG_THROW(psiStateFormulaApFormula.get() != nullptr, storm::exceptions::InvalidPropertyException, "Illegal formula " << *psiStateFormula << " for parametric model checking. Note that only atomic propositions are admitted in that position.");
//
// // Now retrieve the appropriate bitvectors from the atomic propositions.
// storm::storage::BitVector phiStates = phiStateFormulaApFormula->getAp() != "true" ? dtmc.getLabeledStates(phiStateFormulaApFormula->getAp()) : storm::storage::BitVector(dtmc.getNumberOfStates(), true);
// storm::storage::BitVector psiStates = dtmc.getLabeledStates(psiStateFormulaApFormula->getAp());
//
// // Do some sanity checks to establish some required properties.
// STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
//
// // Then, compute the subset of states that has a probability of 0 or 1, respectively.
// std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates);
// storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
// storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
// storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
//
// // If the initial state is known to have either probability 0 or 1, we can directly return the result.
// if (dtmc.getInitialStates().isDisjointFrom(maybeStates)) {
// STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step.");
// return statesWithProbability0.get(*dtmc.getInitialStates().begin()) ? storm::utility::constantZero<storm::RationalFunction>() : storm::utility::constantOne<storm::RationalFunction>();
// }
//
// // Determine the set of states that is reachable from the initial state without jumping over a target state.
// storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, statesWithProbability1);
//
// // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
// maybeStates &= reachableStates;
//
// // Create a vector for the probabilities to go to a state with probability 1 in one step.
// std::vector<storm::RationalFunction> oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
//
// // Determine the set of initial states of the sub-DTMC.
// storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates;
//
// // We then build the submatrix that only has the transitions of the maybe states.
// storm::storage::SparseMatrix<storm::RationalFunction> submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
//
// // To be able to apply heuristics later, we now determine the distance of each state to the initial state.
// std::vector<std::pair<storm::storage::sparse::state_type, std::size_t>> stateQueue;
// stateQueue.reserve(submatrix.getRowCount());
// storm::storage::BitVector statesInQueue(submatrix.getRowCount());
// std::vector<std::size_t> distances(submatrix.getRowCount());
//
// storm::storage::sparse::state_type currentPosition = 0;
// for (auto const& initialState : newInitialStates) {
// stateQueue.emplace_back(initialState, 0);
// statesInQueue.set(initialState);
// }
//
// // Perform a BFS.
// while (currentPosition < stateQueue.size()) {
// std::pair<storm::storage::sparse::state_type, std::size_t> const& stateDistancePair = stateQueue[currentPosition];
// distances[stateDistancePair.first] = stateDistancePair.second;
//
// for (auto const& successorEntry : submatrix.getRow(stateDistancePair.first)) {
// if (!statesInQueue.get(successorEntry.getColumn())) {
// stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1);
// statesInQueue.set(successorEntry.getColumn());
// }
// }
// ++currentPosition;
// }
//
// storm::modelchecker::reachability::SparseSccModelChecker<storm::RationalFunction> modelchecker;
//
// return std::make_tuple(modelchecker.computeReachabilityProbability(submatrix, oneStepProbabilities, submatrix.transpose(), newInitialStates, phiStates, psiStates, distances),submatrix, oneStepProbabilities, newInitialStates, threshold, strict);
//}
template<typename ValueType> template<typename ValueType>
void printApproximateResult(ValueType const& value) { void printApproximateResult(ValueType const& value) {
// Intentionally left empty. // Intentionally left empty.
@ -146,10 +40,15 @@ void check() {
std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString(); std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString();
storm::prism::Program program = storm::parser::PrismParser::parse(programFile); storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
STORM_LOG_THROW(storm::settings::generalSettings().isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to perform model checking without a property.");
std::shared_ptr<storm::logic::Formula> formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty());
boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
if (storm::settings::generalSettings().isPropertySet()) {
formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty());
}
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options(*formula);
typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
if (formula) {
options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
}
options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString()); options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString());
std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options); std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
@ -158,60 +57,57 @@ void check() {
if (model->hasTransitionRewards()) { if (model->hasTransitionRewards()) {
model->convertTransitionRewardsToStateRewards(); model->convertTransitionRewardsToStateRewards();
} }
model->printModelInformationToStream(std::cout);
// Program Translation Time Measurement, End // Program Translation Time Measurement, End
std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl; std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl;
if (model->hasTransitionRewards()) {
model->convertTransitionRewardsToStateRewards();
}
std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
STORM_LOG_THROW(modelchecker.canHandle(*formula), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula << "'.");
model->printModelInformationToStream(std::cout);
std::cout << "Checking formula " << *formula << std::endl;
if (formula) {
STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidArgumentException, "The given model is not a DTMC and, hence, not currently supported.");
std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
bool checkRewards = formula->isRewardOperatorFormula();
storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
STORM_LOG_THROW(modelchecker.canHandle(*formula.get()), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula.get() << "'.");
// Perform bisimulation minimization if requested.
if (storm::settings::generalSettings().isBisimulationSet()) {
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula);
options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
std::cout << "Checking formula " << *formula.get() << std::endl;
storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
*dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
dtmc->printModelInformationToStream(std::cout);
}
assert(dtmc);
storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
constraintCollector(*dtmc);
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula);
ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
if (storm::settings::parametricSettings().exportResultToFile()) {
storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
}
// Report the result.
STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
result->writeToStream(std::cout, model->getInitialStates());
if (std::is_same<ValueType, storm::RationalFunction>::value) {
printApproximateResult(valueFunction);
// Perform bisimulation minimization if requested.
if (storm::settings::generalSettings().isBisimulationSet()) {
typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula.get());
options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
*dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
dtmc->printModelInformationToStream(std::cout);
}
STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong.");
storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
constraintCollector(*dtmc);
std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula.get());
ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
if (storm::settings::parametricSettings().exportResultToFile()) {
storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
}
// Report the result.
STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
result->writeToStream(std::cout, model->getInitialStates());
if (std::is_same<ValueType, storm::RationalFunction>::value) {
printApproximateResult(valueFunction);
}
std::cout << std::endl;
} }
std::cout << std::endl;
} }
/*! /*!
* Main entry point of the executable storm.
* Main entry point of the executable pstorm.
*/ */
int main(const int argc, const char** argv) { int main(const int argc, const char** argv) {
try { try {
@ -227,44 +123,6 @@ int main(const int argc, const char** argv) {
std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now();
std::cout << std::endl << "Total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms." << std::endl << std::endl; std::cout << std::endl << "Total time: " << std::chrono::duration_cast<std::chrono::milliseconds>(totalTimeEnd - totalTimeStart).count() << "ms." << std::endl << std::endl;
// // Perform bisimulation minimization if requested.
// if (storm::settings::generalSettings().isBisimulationSet()) {
// storm::storage::DeterministicModelStrongBisimulationDecomposition<storm::RationalFunction> bisimulationDecomposition(*dtmc, true);
// dtmc = bisimulationDecomposition.getQuotient()->as<storm::models::Dtmc<storm::RationalFunction>>();
//
// dtmc->printModelInformationToStream(std::cout);
// }
// storm::RationalFunction valueFunction2 = modelchecker.computeReachabilityProbability(*dtmc, filterFormula);
// STORM_PRINT_AND_LOG(std::endl << "computed value2 " << valueFunction2 << std::endl);
//
// storm::RationalFunction diff = storm::utility::simplify(valueFunction - valueFunction2);
// STORM_PRINT_AND_LOG(std::endl << "difference: " << diff << std::endl);
// Get variables from parameter definitions in prism program.
// std::set<storm::Variable> parameters;
// for(auto constant : program.getConstants())
// {
// if(!constant.isDefined())
// {
// std::cout << "got undef constant " << constant.getName() << std::endl;
// carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName());
// assert(p != storm::Variable::NO_VARIABLE);
// parameters.insert(p);
// }
// }
// STORM_LOG_ASSERT(parameters == valueFunction.gatherVariables(), "Parameters in result and program definition do not coincide.");
// if(storm::settings::parametricSettings().exportResultToFile()) {
// storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
// }
// if (storm::settings::parametricSettings().exportToSmt2File() && std::get<1>(result) && std::get<2>(result) && std::get<3>(result) && std::get<4>(result) && std::get<5>(result)) {
// storm::modelchecker::reachability::DirectEncoding dec;
// storm::utility::exportStringStreamToFile(dec.encodeAsSmt2(std::get<1>(result).get(), std::get<2>(result).get(), parameters, std::get<3>(result).get(), carl::rationalize<storm::RationalFunction::CoeffType>(std::get<4>(result).get()), std::get<5>(result).get()), "out.smt");
// }
// All operations have now been performed, so we clean up everything and terminate. // All operations have now been performed, so we clean up everything and terminate.
storm::utility::cli::cleanUp(); storm::utility::cli::cleanUp();
return 0; return 0;
@ -273,144 +131,4 @@ int main(const int argc, const char** argv) {
} catch (std::exception const& exception) { } catch (std::exception const& exception) {
STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what()); STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what());
} }
}
//#include <memory>
//#include <stdint.h>
//
//#include "stormParametric.h"
//#include "adapters/ExplicitModelAdapter.h"
//#include "utility/graph.h"
//#include "modelchecker/reachability/DirectEncoding.h"
//#include "storage/BitVector.h"
//#include "storage/DeterministicTransition.h"
//
//using storm::storage::StateId;
//
//namespace storm
//{
//
//
//void ParametricStormEntryPoint::createModel()
//{
// mModel = storm::adapters::ExplicitModelAdapter<RationalFunction>::translateProgram(mProgram, mConstants);
// mModel->printModelInformationToStream(std::cout);
//}
//
//std::string ParametricStormEntryPoint::reachabilityToSmt2(std::string const& label)
//{
//
// storm::storage::BitVector phiStates(mModel->getNumberOfStates(), true);
// storm::storage::BitVector initStates = mModel->getInitialStates();
// storm::storage::BitVector targetStates = mModel->getLabeledStates(label);
//
// std::shared_ptr<models::Dtmc<RationalFunction>> dtmc = mModel->as<models::Dtmc<RationalFunction>>();
// // 1. make target states absorbing.
// dtmc->makeAbsorbing(targetStates);
// // 2. throw away anything which does not add to the reachability probability.
// // 2a. remove non productive states
// storm::storage::BitVector productiveStates = utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, targetStates);
// // 2b. calculate set of states wich
// storm::storage::BitVector almostSurelyReachingTargetStates = ~utility::graph::performProbGreater0(*dtmc, dtmc->getBackwardTransitions(), phiStates, ~productiveStates);
// // 2c. Make such states also target states.
// dtmc->makeAbsorbing(almostSurelyReachingTargetStates);
// // 2d. throw away non reachable states
// storm::storage::BitVector reachableStates = utility::graph::performProbGreater0(*dtmc, dtmc->getTransitionMatrix(), phiStates, initStates);
// storm::storage::BitVector bv = productiveStates & reachableStates;
// dtmc->getStateLabeling().addAtomicProposition("__targets__", targetStates | almostSurelyReachingTargetStates);
// models::Dtmc<RationalFunction> subdtmc = dtmc->getSubDtmc(bv);
//
// phiStates = storm::storage::BitVector(subdtmc.getNumberOfStates(), true);
// initStates = subdtmc.getInitialStates();
// targetStates = subdtmc.getLabeledStates("__targets__");
// storm::storage::BitVector deadlockStates(phiStates);
// deadlockStates.set(subdtmc.getNumberOfStates()-1,false);
//
// // Search for states with only one non-deadlock successor.
// std::map<StateId, storage::DeterministicTransition<RationalFunction>> chainedStates;
// StateId nrStates = subdtmc.getNumberOfStates();
// StateId deadlockState = nrStates - 1;
// for(StateId source = 0; source < nrStates - 1; ++source)
// {
// if(targetStates[source])
// {
// continue;
// }
// storage::DeterministicTransition<RationalFunction> productiveTransition(nrStates);
// for(auto const& transition : subdtmc.getRows(source))
// {
// if(productiveTransition.targetState() == nrStates)
// {
// // first transition.
// productiveTransition = transition;
// }
// else
// {
// // second transition
// if(transition.first != deadlockState)
// {
// productiveTransition.targetState() = nrStates;
// break;
// }
// }
// }
// if(productiveTransition.targetState() != nrStates)
// {
// chainedStates.emplace(source, productiveTransition);
// }
// }
// storage::BitVector eliminatedStates(nrStates, false);
// for(auto & chainedState : chainedStates)
// {
// assert(chainedState.first != chainedState.second.targetState());
// auto it = chainedStates.find(chainedState.second.targetState());
// if(it != chainedStates.end())
// {
// //std::cout << "----------------------------" << std::endl;
// //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl;
// //std::cout << it->first << " -- " << it->second.probability() << " --> " << it->second.targetState() << std::endl;
// chainedState.second.targetState() = it->second.targetState();
// chainedState.second.probability() *= it->second.probability();
// //std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl;
// //std::cout << "----------------------------" << std::endl;
// chainedStates.erase(it);
// eliminatedStates.set(it->first, true);
// }
// }
//
//
// for(auto chainedState : chainedStates)
// {
// if(!eliminatedStates[chainedState.first])
// {
// std::cout << chainedState.first << " -- " << chainedState.second.probability() << " --> " << chainedState.second.targetState() << std::endl;
// }
// }
//
// storage::StronglyConnectedComponentDecomposition<RationalFunction> sccs(subdtmc);
// std::cout << sccs << std::endl;
//
// modelchecker::reachability::DirectEncoding dec;
// std::vector<carl::Variable> parameters;
// return dec.encodeAsSmt2(subdtmc, parameters, subdtmc.getLabeledStates("init"), subdtmc.getLabeledStates("__targets__"), mpq_class(1,2));
//
//}
//
//
//void storm_parametric(const std::string& constants, const storm::prism::Program& program)
//{
// ParametricStormEntryPoint entry(constants, program);
// entry.createModel();
// storm::settings::Settings* s = storm::settings::Settings::getInstance();
// if(s->isSet("reachability"))
// {
// std::ofstream fstream("test.smt2");
// fstream << entry.reachabilityToSmt2(s->getOptionByLongName("reachability").getArgument(0).getValueAsString());
// fstream.close();
// }
//
//
//}
//
//}
}

8
src/utility/cli.h
View File

@ -129,7 +129,7 @@ namespace storm {
* Prints the header including information about the linked libraries. * Prints the header including information about the linked libraries.
*/ */
void printHeader(const int argc, const char* argv[]) { void printHeader(const int argc, const char* argv[]) {
std::cout << "PROPhESY" << std::endl;
std::cout << "StoRM" << std::endl;
std::cout << "--------" << std::endl << std::endl; std::cout << "--------" << std::endl << std::endl;
@ -138,7 +138,7 @@ namespace storm {
std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
#endif #endif
#ifdef STORM_HAVE_GLPK #ifdef STORM_HAVE_GLPK
// std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
#endif #endif
#ifdef STORM_HAVE_GUROBI #ifdef STORM_HAVE_GUROBI
std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl; std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
@ -160,7 +160,7 @@ namespace storm {
commandStream << argv[i] << " "; commandStream << argv[i] << " ";
} }
std::cout << "Command line arguments: " << commandStream.str() << std::endl; std::cout << "Command line arguments: " << commandStream.str() << std::endl;
// std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
} }
@ -218,8 +218,6 @@ namespace storm {
storm::settings::SettingsManager& manager = storm::settings::mutableManager(); storm::settings::SettingsManager& manager = storm::settings::mutableManager();
try { try {
manager.setFromCommandLine(argc, argv); manager.setFromCommandLine(argc, argv);
// std::vector<std::string> arguments = {"--symbolic", "/Users/chris/work/prism-trunk/prism-examples/self-stabilisation/herman/herman7.mod", "--prop", "R=? [F \"stable\"]"};
// manager.setFromExplodedString(arguments);
} catch (storm::exceptions::OptionParserException& e) { } catch (storm::exceptions::OptionParserException& e) {
manager.printHelp(); manager.printHelp();
throw e; throw e;

Write Preview
Loading…
Cancel
Save