sjunges
11 years ago
13 changed files with 260 additions and 241 deletions
-
2src/adapters/ExplicitModelAdapter.h
-
6src/adapters/extendedCarl.h
-
9src/exceptions/ExceptionMacros.h
-
22src/extensions/parameters/main.cpp
-
2src/parser/DeterministicModelParser.cpp
-
37src/parser/DeterministicSparseTransitionParser.cpp
-
4src/parser/DeterministicSparseTransitionParser.h
-
4src/parser/ReadValues.h
-
23src/storage/expressions/ExpressionEvaluation.h
-
6src/storm.cpp
-
294src/stormParametric.cpp
-
66src/stormParametric.h
-
24test/functional/parser/DeterministicSparseTransitionParserTest.cpp
@ -0,0 +1,22 @@ |
|||
//
|
|||
//int main(const int argc, const char* argv[]) {
|
|||
// // Print an information header.
|
|||
// //printHeader(argc, argv);
|
|||
//
|
|||
// // Initialize the logging engine and perform other initalizations.
|
|||
// initializeLogger();
|
|||
// setUp();
|
|||
//
|
|||
// // Program Translation Time Measurement, Start
|
|||
// std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now();
|
|||
//
|
|||
// // First, we build the model using the given symbolic model description and constant definitions.
|
|||
// std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString();
|
|||
// std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString();
|
|||
// storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
|
|||
//
|
|||
// // Program Translation Time Measurement, End
|
|||
// std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
|
|||
// std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl;
|
|||
// storm_parametric(constants, program);
|
|||
//}
|
|||
@ -1,148 +1,148 @@ |
|||
#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;
|
|||
//#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;
|
|||
//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; |
|||
for(auto constant : mProgram.getConstants()) |
|||
{ |
|||
if(!constant.isDefined()) |
|||
{ |
|||
std::cout << constant.getName() << std::endl; |
|||
carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName()); |
|||
assert(p != carl::Variable::NO_VARIABLE); |
|||
parameters.push_back(p); |
|||
} |
|||
} |
|||
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(); |
|||
} |
|||
|
|||
|
|||
} |
|||
|
|||
} |
|||
// }
|
|||
// }
|
|||
//
|
|||
// storage::StronglyConnectedComponentDecomposition<RationalFunction> sccs(subdtmc);
|
|||
// std::cout << sccs << std::endl;
|
|||
//
|
|||
// modelchecker::reachability::DirectEncoding dec;
|
|||
// std::vector<carl::Variable> parameters;
|
|||
// for(auto constant : mProgram.getConstants())
|
|||
// {
|
|||
// if(!constant.isDefined())
|
|||
// {
|
|||
// std::cout << constant.getName() << std::endl;
|
|||
// carl::Variable p = carl::VariablePool::getInstance().findVariableWithName(constant.getName());
|
|||
// assert(p != carl::Variable::NO_VARIABLE);
|
|||
// parameters.push_back(p);
|
|||
// }
|
|||
// }
|
|||
// 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();
|
|||
// }
|
|||
//
|
|||
//
|
|||
//}
|
|||
//
|
|||
//}
|
|||
@ -1,33 +1,33 @@ |
|||
|
|||
|
|||
|
|||
#pragma once |
|||
#include "storage/prism/Program.h" |
|||
#include "models/AbstractModel.h" |
|||
#include "storage/parameters.h" |
|||
|
|||
namespace storm |
|||
{ |
|||
class ParametricStormEntryPoint |
|||
{ |
|||
private: |
|||
std::string const& mConstants; |
|||
storm::prism::Program const& mProgram; |
|||
std::shared_ptr<storm::models::AbstractModel<RationalFunction>> mModel; |
|||
public: |
|||
ParametricStormEntryPoint(std::string const& constants, storm::prism::Program const& program) : |
|||
mConstants(constants), |
|||
mProgram(program) |
|||
{ |
|||
|
|||
} |
|||
|
|||
void createModel(); |
|||
std::string reachabilityToSmt2(std::string const&); |
|||
|
|||
virtual ~ParametricStormEntryPoint() {} |
|||
|
|||
}; |
|||
void storm_parametric(std::string const& constants, storm::prism::Program const&); |
|||
} |
|||
|
|||
// |
|||
// |
|||
// |
|||
//#pragma once |
|||
//#include "storage/prism/Program.h" |
|||
//#include "models/AbstractModel.h" |
|||
//#include "storage/parameters.h" |
|||
// |
|||
//namespace storm |
|||
//{ |
|||
// class ParametricStormEntryPoint |
|||
// { |
|||
// private: |
|||
// std::string const& mConstants; |
|||
// storm::prism::Program const& mProgram; |
|||
// std::shared_ptr<storm::models::AbstractModel<RationalFunction>> mModel; |
|||
// public: |
|||
// ParametricStormEntryPoint(std::string const& constants, storm::prism::Program const& program) : |
|||
// mConstants(constants), |
|||
// mProgram(program) |
|||
// { |
|||
// |
|||
// } |
|||
// |
|||
// void createModel(); |
|||
// std::string reachabilityToSmt2(std::string const&); |
|||
// |
|||
// virtual ~ParametricStormEntryPoint() {} |
|||
// |
|||
// }; |
|||
// void storm_parametric(std::string const& constants, storm::prism::Program const&); |
|||
//} |
|||
// |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue