Browse Source

Merge remote-tracking branch 'origin' into gamebased

main
dehnert 7 years ago
parent
commit
d09bcc2e3b
  1. 554
      resources/examples/testfiles/ctmc/cluster2.drn
  2. 32337
      resources/examples/testfiles/dtmc/crowds-5-5.drn
  3. 71
      resources/examples/testfiles/ma/jobscheduler.drn
  4. 2
      resources/examples/testfiles/mdp/two_dice.drn
  5. 21
      src/storm-cli-utilities/model-handling.h
  6. 2
      src/storm/modelchecker/CheckTask.h
  7. 4
      src/storm/modelchecker/results/CheckResult.cpp
  8. 4
      src/storm/modelchecker/results/CheckResult.h
  9. 2
      src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h
  10. 4
      src/storm/models/sparse/Model.cpp
  11. 144
      src/storm/parser/DirectEncodingParser.cpp
  12. 20
      src/storm/parser/MarkovAutomatonParser.cpp
  13. 4
      src/storm/settings/modules/CoreSettings.cpp
  14. 2
      src/storm/settings/modules/CoreSettings.h
  15. 6
      src/storm/storage/Scheduler.h
  16. 2
      src/storm/storage/prism/Program.cpp
  17. 45
      src/storm/utility/DirectEncodingExporter.cpp
  18. 4
      src/storm/utility/DirectEncodingExporter.h
  19. 33
      src/storm/utility/constants.cpp
  20. 54
      src/test/storm/parser/DirectEncodingParserTest.cpp
  21. 4
      travis/build_helper.sh

554
resources/examples/testfiles/ctmc/cluster2.drn
File diff suppressed because it is too large
View File

32337
resources/examples/testfiles/dtmc/crowds-5-5.drn
File diff suppressed because it is too large
View File

71
resources/examples/testfiles/ma/jobscheduler.drn

@ -0,0 +1,71 @@
// Exported by storm
// Original model type: Markov Automaton
@type: Markov Automaton
@parameters
@reward_models
avg_waiting_time
@nr_states
17
@model
state 0 !0 [1] init
action 0 [0]
1 : 1
action 1 [0]
2 : 1
action 2 [0]
3 : 1
state 1 !3 [1]
action 0 [0]
4 : 0.333333
5 : 0.666667
state 2 !4 [1]
action 0 [0]
4 : 0.25
6 : 0.75
state 3 !5 [1]
action 0 [0]
5 : 0.4
6 : 0.6
state 4 !0 [0.666667] one_job_finished slowest_before_fastest
action 0 [0]
7 : 1
state 5 !0 [0.666667] one_job_finished
action 0 [0]
8 : 1
state 6 !0 [0.666667] one_job_finished
action 0 [0]
9 : 1
state 7 !5 [0.666667] one_job_finished slowest_before_fastest
action 0 [0]
10 : 0.4
11 : 0.6
state 8 !4 [0.666667] one_job_finished
action 0 [0]
10 : 0.25
12 : 0.75
state 9 !3 [0.666667] one_job_finished
action 0 [0]
11 : 0.333333
12 : 0.666667
state 10 !0 [0.333333] half_of_jobs_finished slowest_before_fastest
action 0 [0]
13 : 1
state 11 !0 [0.333333] half_of_jobs_finished
action 0 [0]
14 : 1
state 12 !0 [0.333333] half_of_jobs_finished
action 0 [0]
15 : 1
state 13 !3 [0.333333] half_of_jobs_finished slowest_before_fastest
action 0 [0]
16 : 1
state 14 !2 [0.333333] half_of_jobs_finished
action 0 [0]
16 : 1
state 15 !1 [0.333333] half_of_jobs_finished
action 0 [0]
16 : 1
state 16 !1 [0] all_jobs_finished deadlock
action 0 [0]
16 : 1

2
resources/examples/testfiles/mdp/two_dice.drn

@ -3,6 +3,8 @@
@type: MDP
@parameters
@reward_models
coinflips
@nr_states
169
@model

21
src/storm-cli-utilities/model-handling.h

@ -217,7 +217,7 @@ namespace storm {
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
std::shared_ptr<storm::models::ModelBase> result;
if (input.model) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
result = buildModelDd<DdType, ValueType>(input);
} else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
result = buildModelSparse<ValueType>(input, buildSettings);
@ -350,6 +350,25 @@ namespace storm {
result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
}
if (result && result->first->isSymbolicModel() && storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::DdSparse) {
// Mark as changed.
result->second = true;
std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel = result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
if (symbolicModel->isOfType(storm::models::ModelType::Dtmc)) {
storm::transformer::SymbolicDtmcToSparseDtmcTransformer<DdType, ExportValueType> transformer;
result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<DdType, ExportValueType>>());
} else if (symbolicModel->isOfType(storm::models::ModelType::Ctmc)) {
storm::transformer::SymbolicCtmcToSparseCtmcTransformer<DdType, ExportValueType> transformer;
result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<DdType, ExportValueType>>());
} else if (symbolicModel->isOfType(storm::models::ModelType::Mdp)) {
storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ExportValueType> transformer;
result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Mdp<DdType, ExportValueType>>());
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
}
}
return *result;
}

2
src/storm/modelchecker/CheckTask.h

@ -211,7 +211,7 @@ namespace storm {
/*!
* Sets whether to produce schedulers (if supported).
*/
void setProduceSchedulers(bool produceSchedulers) {
void setProduceSchedulers(bool produceSchedulers = true) {
this->produceSchedulers = produceSchedulers;
}

4
src/storm/modelchecker/results/CheckResult.cpp

@ -162,6 +162,10 @@ namespace storm {
SymbolicParetoCurveCheckResult<Type, ValueType> const& CheckResult::asSymbolicParetoCurveCheckResult() const {
return dynamic_cast<SymbolicParetoCurveCheckResult<Type, ValueType> const&>(*this);
}
bool CheckResult::hasScheduler() const {
return false;
}
// Explicitly instantiate the template functions.
template QuantitativeCheckResult<double>& CheckResult::asQuantitativeCheckResult();

4
src/storm/modelchecker/results/CheckResult.h

@ -111,7 +111,9 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult<Type, ValueType> const& asSymbolicParetoCurveCheckResult() const;
virtual bool hasScheduler() const;
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
};

2
src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.h

@ -65,7 +65,7 @@ namespace storm {
virtual ValueType average() const override;
virtual ValueType sum() const override;
bool hasScheduler() const;
virtual bool hasScheduler() const override;
void setScheduler(std::unique_ptr<storm::storage::Scheduler<ValueType>>&& scheduler);
storm::storage::Scheduler<ValueType> const& getScheduler() const;
storm::storage::Scheduler<ValueType>& getScheduler();

4
src/storm/models/sparse/Model.cpp

@ -74,9 +74,9 @@ namespace storm {
STORM_LOG_THROW(!components.exitRates.is_initialized() || components.exitRates->size() == stateCount, storm::exceptions::IllegalArgumentException, "Size of exit rate vector does not match state count.");
STORM_LOG_THROW(this->isOfType(ModelType::Ctmc) || components.markovianStates.is_initialized(), storm::exceptions::IllegalArgumentException, "Can not create Markov Automaton: no Markovian states given.");
} else {
STORM_LOG_ERROR_COND(!components.rateTransitions && !components.exitRates.is_initialized(), "Rates specified for discrete-time model. The rates will be ignored.");
STORM_LOG_WARN_COND(!components.rateTransitions && !components.exitRates.is_initialized(), "Rates specified for discrete-time model. The rates will be ignored.");
}
STORM_LOG_ERROR_COND(this->isOfType(ModelType::MarkovAutomaton) || !components.markovianStates.is_initialized(), "Markovian states given for a model that is not a Markov automaton (will be ignored).");
STORM_LOG_WARN_COND(this->isOfType(ModelType::MarkovAutomaton) || !components.markovianStates.is_initialized(), "Markovian states given for a model that is not a Markov automaton (will be ignored).");
}
template<typename ValueType, typename RewardModelType>

144
src/storm/parser/DirectEncodingParser.cpp

@ -40,26 +40,26 @@ namespace storm {
bool sawParameters = false;
size_t nrStates = 0;
storm::models::ModelType type;
std::vector<std::string> rewardModelNames;
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents;
std::shared_ptr<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>> modelComponents;
// Parse header
while(std::getline(file, line)) {
if(line.empty() || boost::starts_with(line, "//")) {
while (std::getline(file, line)) {
if (line.empty() || boost::starts_with(line, "//")) {
continue;
}
if (boost::starts_with(line, "@type: ")) {
// Parse type
STORM_LOG_THROW(!sawType, storm::exceptions::WrongFormatException, "Type declared twice");
type = storm::models::getModelType(line.substr(7));
STORM_LOG_TRACE("Model type: " << type);
STORM_LOG_THROW(type != storm::models::ModelType::MarkovAutomaton, storm::exceptions::NotSupportedException, "Markov Automata in DRN format are not supported (unclear indication of Markovian Choices in DRN format)");
STORM_LOG_THROW(type != storm::models::ModelType::S2pg, storm::exceptions::NotSupportedException, "Stochastic Two Player Games in DRN format are not supported.");
sawType = true;
}
if(line == "@parameters") {
} else if (line == "@parameters") {
// Parse parameters
STORM_LOG_THROW(!sawParameters, storm::exceptions::WrongFormatException, "Parameters declared twice");
std::getline(file, line);
if (line != "") {
std::vector<std::string> parameters;
@ -70,26 +70,28 @@ namespace storm {
}
}
sawParameters = true;
}
if(line == "@reward_models") {
} else if (line == "@reward_models") {
// Parse reward models
STORM_LOG_THROW(rewardModelNames.size() == 0, storm::exceptions::WrongFormatException, "Reward model names declared twice");
std::getline(file, line);
boost::split(rewardModelNames, line, boost::is_any_of("\t "));
}
if(line == "@nr_states") {
} else if (line == "@nr_states") {
// Parse no. of states
STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice");
std::getline(file, line);
nrStates = NumberParser<size_t>::parse(line);
}
if(line == "@model") {
} else if (line == "@model") {
// Parse rest of the model
STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model.");
STORM_LOG_THROW(sawParameters, storm::exceptions::WrongFormatException, "Parameters have to be declared before model.");
STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "Nr States has to be declared before model.");
STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "No. of states has to be declared before model.");
// Construct model components
modelComponents = parseStates(file, type, nrStates, valueParser, rewardModelNames);
break;
} else {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse line '" << line << "'.");
}
}
// Done parsing
@ -104,15 +106,21 @@ namespace storm {
// Initialize
auto modelComponents = std::make_shared<storm::storage::sparse::ModelComponents<ValueType, RewardModelType>>();
bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton);
bool continousTime = (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton);
storm::storage::SparseMatrixBuilder<ValueType> builder = storm::storage::SparseMatrixBuilder<ValueType>(0, 0, 0, false, nonDeterministic, 0);
modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize);
std::vector<std::vector<ValueType>> stateRewards;
if (continousTime) {
modelComponents->exitRates = std::vector<ValueType>(stateSize);
if (type == storm::models::ModelType::MarkovAutomaton) {
modelComponents->markovianStates = storm::storage::BitVector(stateSize);
}
}
// We parse rates for continuous time models.
if (type == storm::models::ModelType::Ctmc) {
modelComponents->rateTransitions = true;
}
// Iterate over all lines
std::string line;
size_t row = 0;
@ -128,34 +136,66 @@ namespace storm {
} else {
++state;
}
line = line.substr(6);
size_t parsedId;
size_t posId = line.find(" ");
if (posId != std::string::npos) {
parsedId = NumberParser<size_t>::parse(line.substr(0, posId));
// Parse rewards and labels
line = line.substr(posId+1);
// Check for rewards
if (boost::starts_with(line, "[")) {
// Rewards found
size_t posEndReward = line.find(']');
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
std::string rewardsStr = line.substr(1, posEndReward-1);
STORM_LOG_TRACE("State rewards: " << rewardsStr);
std::vector<std::string> rewards;
boost::split(rewards, rewardsStr, boost::is_any_of(","));
if (stateRewards.size() < rewards.size()) {
stateRewards.resize(rewards.size(), std::vector<ValueType>(stateSize, storm::utility::zero<ValueType>()));
}
auto stateRewardsIt = stateRewards.begin();
for (auto const& rew : rewards) {
(*stateRewardsIt)[state] = valueParser.parseValue(rew);
++stateRewardsIt;
}
line = line.substr(posEndReward+1);
STORM_LOG_TRACE("New state " << state);
// Parse state id
line = line.substr(6); // Remove "state "
std::string curString = line;
size_t posEnd = line.find(" ");
if (posEnd != std::string::npos) {
curString = line.substr(0, posEnd);
line = line.substr(posEnd+1);
} else {
line = "";
}
size_t parsedId = NumberParser<size_t>::parse(curString);
STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond.");
if (nonDeterministic) {
STORM_LOG_TRACE("new Row Group starts at " << row << ".");
builder.newRowGroup(row);
}
if (type == storm::models::ModelType::Ctmc || type == storm::models::ModelType::MarkovAutomaton) {
// Parse exit rate for CTMC or MA
STORM_LOG_THROW(boost::starts_with(line, "!"), storm::exceptions::WrongFormatException, "Exit rate missing.");
line = line.substr(1); //Remove "!"
curString = line;
posEnd = line.find(" ");
if (posEnd != std::string::npos) {
curString = line.substr(0, posEnd);
line = line.substr(posEnd+1);
} else {
line = "";
}
ValueType exitRate = valueParser.parseValue(curString);
if (type == storm::models::ModelType::MarkovAutomaton && !storm::utility::isZero<ValueType>(exitRate)) {
modelComponents->markovianStates.get().set(state);
}
STORM_LOG_TRACE("Exit rate " << exitRate);
modelComponents->exitRates.get()[state] = exitRate;
}
if (boost::starts_with(line, "[")) {
// Parse rewards
size_t posEndReward = line.find(']');
STORM_LOG_THROW(posEndReward != std::string::npos, storm::exceptions::WrongFormatException, "] missing.");
std::string rewardsStr = line.substr(1, posEndReward-1);
STORM_LOG_TRACE("State rewards: " << rewardsStr);
std::vector<std::string> rewards;
boost::split(rewards, rewardsStr, boost::is_any_of(","));
if (stateRewards.size() < rewards.size()) {
stateRewards.resize(rewards.size(), std::vector<ValueType>(stateSize, storm::utility::zero<ValueType>()));
}
auto stateRewardsIt = stateRewards.begin();
for (auto const& rew : rewards) {
(*stateRewardsIt)[state] = valueParser.parseValue(rew);
++stateRewardsIt;
}
// Check for labels
line = line.substr(posEndReward+1);
}
// Parse labels
if (!line.empty()) {
std::vector<std::string> labels;
boost::split(labels, line, boost::is_any_of(" "));
for (std::string label : labels) {
@ -163,18 +203,10 @@ namespace storm {
modelComponents->stateLabeling.addLabel(label);
}
modelComponents->stateLabeling.addLabelToState(label, state);
STORM_LOG_TRACE("New label: " << label);
STORM_LOG_TRACE("New label: '" << label << "'");
}
} else {
// Only state id given
parsedId = NumberParser<size_t>::parse(line);
}
STORM_LOG_TRACE("New state " << state);
STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond.");
if (nonDeterministic) {
STORM_LOG_TRACE("new Row Group starts at " << row << ".");
builder.newRowGroup(row);
}
} else if (boost::starts_with(line, "\taction ")) {
// New action
if (firstAction) {
@ -182,8 +214,8 @@ namespace storm {
} else {
++row;
}
line = line.substr(8);
STORM_LOG_TRACE("New action: " << row);
line = line.substr(8); //Remove "\taction "
// Check for rewards
if (boost::starts_with(line, "[")) {
// Rewards found

20
src/storm/parser/MarkovAutomatonParser.cpp

@ -25,36 +25,36 @@ namespace storm {
// Parse the state labeling.
storm::models::sparse::StateLabeling resultLabeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename));
// Cunstruct the result components
storm::storage::sparse::ModelComponents<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>> componets(std::move(transitionMatrix), std::move(resultLabeling));
componets.rateTransitions = true;
componets.markovianStates = std::move(transitionResult.markovianStates);
componets.exitRates = std::move(transitionResult.exitRates);
// Construct the result components
storm::storage::sparse::ModelComponents<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>> components(std::move(transitionMatrix), std::move(resultLabeling));
components.rateTransitions = true;
components.markovianStates = std::move(transitionResult.markovianStates);
components.exitRates = std::move(transitionResult.exitRates);
// If given, parse the state rewards file.
boost::optional<std::vector<RewardValueType>> stateRewards;
if (!stateRewardFilename.empty()) {
stateRewards.reset(storm::parser::SparseStateRewardParser<RewardValueType>::parseSparseStateReward(componets.transitionMatrix.getColumnCount(), stateRewardFilename));
stateRewards.reset(storm::parser::SparseStateRewardParser<RewardValueType>::parseSparseStateReward(components.transitionMatrix.getColumnCount(), stateRewardFilename));
}
// Only parse transition rewards if a file is given.
boost::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards;
if (!transitionRewardFilename.empty()) {
transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser<RewardValueType>::parseNondeterministicTransitionRewards(transitionRewardFilename, componets.transitionMatrix));
transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser<RewardValueType>::parseNondeterministicTransitionRewards(transitionRewardFilename, components.transitionMatrix));
}
if (stateRewards || transitionRewards) {
componets.rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<RewardValueType>(std::move(stateRewards), boost::none, std::move(transitionRewards))));
components.rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel<RewardValueType>(std::move(stateRewards), boost::none, std::move(transitionRewards))));
}
// Only parse choice labeling if a file is given.
boost::optional<storm::models::sparse::ChoiceLabeling> choiceLabeling;
if (!choiceLabelingFilename.empty()) {
componets.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(componets.transitionMatrix.getRowCount(), choiceLabelingFilename, componets.transitionMatrix.getRowGroupIndices());
components.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(components.transitionMatrix.getRowCount(), choiceLabelingFilename, components.transitionMatrix.getRowGroupIndices());
}
// generate the Markov Automaton.
return storm::models::sparse::MarkovAutomaton<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>> (std::move(componets));
return storm::models::sparse::MarkovAutomaton<ValueType, storm::models::sparse::StandardRewardModel<RewardValueType>> (std::move(components));
}
template class MarkovAutomatonParser<double, double>;

4
src/storm/settings/modules/CoreSettings.cpp

@ -39,7 +39,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model.").setShortName(counterexampleOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
std::vector<std::string> engines = {"sparse", "hybrid", "dd", "expl", "abs"};
std::vector<std::string> engines = {"sparse", "hybrid", "dd", "dd-to-sparse", "expl", "abs"};
this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build());
@ -164,6 +164,8 @@ namespace storm {
engine = CoreSettings::Engine::Hybrid;
} else if (engineStr == "dd") {
engine = CoreSettings::Engine::Dd;
} else if (engineStr == "dd-to-sparse") {
engine = CoreSettings::Engine::DdSparse;
} else if (engineStr == "expl") {
engine = CoreSettings::Engine::Exploration;
} else if (engineStr == "abs") {

2
src/storm/settings/modules/CoreSettings.h

@ -28,7 +28,7 @@ namespace storm {
public:
// An enumeration of all engines.
enum class Engine {
Sparse, Hybrid, Dd, Exploration, AbstractionRefinement
Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement
};
/*!

6
src/storm/storage/Scheduler.h

@ -44,10 +44,10 @@ namespace storm {
void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0);
/*!
* Sets the choice defined by the scheduler for the given model and memory state.
* Gets the choice defined by the scheduler for the given model and memory state.
*
* @param state The state for which to set the choice.
* @param choice The choice to set for the given state.
* @param state The state for which to get the choice.
* @param memoryState the memory state which we consider.
*/
SchedulerChoice<ValueType> const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const;

2
src/storm/storage/prism/Program.cpp

@ -1124,7 +1124,7 @@ namespace storm {
if (this->getModelType() == Program::ModelType::DTMC || this->getModelType() == Program::ModelType::MDP) {
STORM_LOG_THROW(!hasMarkovianCommand, storm::exceptions::WrongFormatException, "Discrete-time model must not have Markovian commands.");
} else if (this->getModelType() == Program::ModelType::CTMC) {
STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException, "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn on the PRISM compatibility mode using the appropriate flag.");
STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException, "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn on the PRISM compatibility mode using the flag '-pc'.");
}
// Now check the reward models.

45
src/storm/utility/DirectEncodingExporter.cpp

@ -21,20 +21,17 @@ namespace storm {
// Notice that for CTMCs we write the rate matrix instead of probabilities
// Initialize
storm::models::ModelType type = sparseModel->getType();
std::vector<ValueType> exitRates; // Only for CTMCs and MAs.
if(sparseModel->getType() == storm::models::ModelType::Ctmc) {
if (sparseModel->getType() == storm::models::ModelType::Ctmc) {
exitRates = sparseModel->template as<storm::models::sparse::Ctmc<ValueType>>()->getExitRateVector();
} else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) {
type = storm::models::ModelType::Mdp;
STORM_LOG_WARN("Markov automaton is exported as MDP (indication of Markovian choices is not supported in DRN format).");
} else if (sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) {
exitRates = sparseModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates();
}
// Write header
os << "// Exported by storm" << std::endl;
os << "// Original model type: " << sparseModel->getType() << std::endl;
os << "@type: " << type << std::endl;
os << "@type: " << sparseModel->getType() << std::endl;
os << "@parameters" << std::endl;
if (parameters.empty()) {
for (std::string const& parameter : getParameters(sparseModel)) {
@ -55,10 +52,16 @@ namespace storm {
os << "@model" << std::endl;
storm::storage::SparseMatrix<ValueType> const& matrix = sparseModel->getTransitionMatrix();
// Iterate over states and export state information and outgoing transitions
for (typename storm::storage::SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) {
os << "state " << group;
// Write exit rates for CTMCs and MAs
if (!exitRates.empty()) {
os << " !" << exitRates.at(group);
}
// Write state rewards
bool first = true;
for (auto const& rewardModelEntry : sparseModel->getRewardModels()) {
@ -92,22 +95,23 @@ namespace storm {
// Iterate over all actions
for (typename storm::storage::SparseMatrix<ValueType>::index_type row = start; row < end; ++row) {
// Print the actual row.
// Write choice
if (sparseModel->hasChoiceLabeling()) {
os << "\taction ";
bool lfirst = true;
for (auto const& label : sparseModel->getChoiceLabeling().getLabelsOfChoice(row)) {
if (!lfirst) {
os << "_";
lfirst = false;
}
os << label;
lfirst = false;
}
} else {
os << "\taction " << row - start;
}
// Write action rewards
bool first = true;
// Write transition rewards
for (auto const& rewardModelEntry : sparseModel->getRewardModels()) {
if (first) {
os << " [";
@ -116,7 +120,7 @@ namespace storm {
os << ", ";
}
if(rewardModelEntry.second.hasStateActionRewards()) {
if (rewardModelEntry.second.hasStateActionRewards()) {
os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(row));
} else {
os << "0";
@ -126,19 +130,18 @@ namespace storm {
if (!first) {
os << "]";
}
os << std::endl;
// Write probabilities
for(auto it = matrix.begin(row); it != matrix.end(row); ++it) {
// Write transitions
for (auto it = matrix.begin(row); it != matrix.end(row); ++it) {
ValueType prob = it->getValue();
os << "\t\t" << it->getColumn() << " : ";
os << storm::utility::to_string(prob) << std::endl;
}
}
} // end matrix iteration
} // end state iteration
}
template<typename ValueType>
@ -146,9 +149,6 @@ namespace storm {
return {};
}
template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters);
#ifdef STORM_HAVE_CARL
template<>
std::vector<std::string> getParameters(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel) {
std::vector<std::string> parameters;
@ -167,8 +167,9 @@ namespace storm {
return parameters;
}
// Template instantiations
template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters);
template void explicitExportSparseModel<storm::RationalNumber>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> sparseModel, std::vector<std::string> const& parameters);
template void explicitExportSparseModel<storm::RationalFunction>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel, std::vector<std::string> const& parameters);
#endif
}
}

4
src/storm/utility/DirectEncodingExporter.h

@ -18,13 +18,13 @@ namespace storm {
void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters);
/*!
* Accumalate parameters in the model.
* Accumulate parameters in the model.
*
* @param sparseModel Model.
* @return List of parameters in the model.
*/
template<typename ValueType>
std::vector<std::string> getParameters(std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel);
}
}

33
src/storm/utility/constants.cpp

@ -163,13 +163,26 @@ namespace storm {
template<typename ValueType>
ValueType minimum(std::vector<ValueType> const& values) {
return minmax(values).first;
assert(!values.empty());
ValueType min = values.front();
for (auto const& vt : values) {
if (vt < min) {
min = vt;
}
}
return min;
}
template<typename ValueType>
ValueType maximum(std::vector<ValueType> const& values) {
return minmax(values).second;
assert(!values.empty());
ValueType max = values.front();
for (auto const& vt : values) {
if (vt > max) {
max = vt;
}
}
return max;
}
template<typename K, typename ValueType>
@ -896,7 +909,7 @@ namespace storm {
template bool isZero(int const& value);
template bool isConstant(int const& value);
template bool isInfinity(int const& value);
// uint32_t
template uint32_t one();
template uint32_t zero();
@ -905,7 +918,7 @@ namespace storm {
template bool isZero(uint32_t const& value);
template bool isConstant(uint32_t const& value);
template bool isInfinity(uint32_t const& value);
// storm::storage::sparse::state_type
template storm::storage::sparse::state_type one();
template storm::storage::sparse::state_type zero();
@ -914,11 +927,11 @@ namespace storm {
template bool isZero(storm::storage::sparse::state_type const& value);
template bool isConstant(storm::storage::sparse::state_type const& value);
template bool isInfinity(storm::storage::sparse::state_type const& value);
// other instantiations
template unsigned long convertNumber(long const&);
template double convertNumber(long const&);
#if defined(STORM_HAVE_CLN)
// Instantiations for (CLN) rational number.
template storm::ClnRationalNumber one();
@ -942,7 +955,7 @@ namespace storm {
template storm::ClnRationalNumber min(storm::ClnRationalNumber const& first, storm::ClnRationalNumber const& second);
template std::string to_string(storm::ClnRationalNumber const& value);
#endif
#if defined(STORM_HAVE_GMP)
// Instantiations for (GMP) rational number.
template storm::GmpRationalNumber one();
@ -965,10 +978,10 @@ namespace storm {
template storm::GmpRationalNumber min(storm::GmpRationalNumber const& first, storm::GmpRationalNumber const& second);
template std::string to_string(storm::GmpRationalNumber const& value);
#endif
#if defined(STORM_HAVE_CARL) && defined(STORM_HAVE_GMP) && defined(STORM_HAVE_CLN)
#endif
#ifdef STORM_HAVE_CARL
// Instantiations for rational function.
template RationalFunction one();

54
src/test/storm/parser/DirectEncodingParserTest.cpp

@ -1,23 +1,24 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "storm/parser/DirectEncodingParser.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/parser/DirectEncodingParser.h"
#include "storm/models/sparse/MarkovAutomaton.h"
TEST(DirectEncodingParserTest, CtmcParsing) {
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.drn");
TEST(DirectEncodingParserTest, DtmcParsing) {
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.drn");
// Test if parsed correctly.
ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType());
ASSERT_EQ(276ul, modelPtr->getNumberOfStates());
ASSERT_EQ(1120ul, modelPtr->getNumberOfTransitions());
ASSERT_EQ(storm::models::ModelType::Dtmc, modelPtr->getType());
ASSERT_EQ(8607ul, modelPtr->getNumberOfStates());
ASSERT_EQ(15113ul, modelPtr->getNumberOfTransitions());
ASSERT_TRUE(modelPtr->hasLabel("init"));
ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasLabel("premium"));
ASSERT_EQ(64ul, modelPtr->getStates("premium").getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasLabel("minimum"));
ASSERT_EQ(132ul, modelPtr->getStates("minimum").getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasLabel("observeIGreater1"));
ASSERT_EQ(4650ul, modelPtr->getStates("observeIGreater1").getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasLabel("observe0Greater1"));
ASSERT_EQ(1260ul, modelPtr->getStates("observe0Greater1").getNumberOfSetBits());
}
TEST(DirectEncodingParserTest, MdpParsing) {
@ -36,3 +37,36 @@ TEST(DirectEncodingParserTest, MdpParsing) {
ASSERT_EQ(2ul, modelPtr->getStates("eleven").getNumberOfSetBits());
}
TEST(DirectEncodingParserTest, CtmcParsing) {
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.drn");
// Test if parsed correctly.
ASSERT_EQ(storm::models::ModelType::Ctmc, modelPtr->getType());
ASSERT_EQ(276ul, modelPtr->getNumberOfStates());
ASSERT_EQ(1120ul, modelPtr->getNumberOfTransitions());
ASSERT_TRUE(modelPtr->hasLabel("init"));
ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasLabel("premium"));
ASSERT_EQ(64ul, modelPtr->getStates("premium").getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasLabel("minimum"));
ASSERT_EQ(132ul, modelPtr->getStates("minimum").getNumberOfSetBits());
}
TEST(DirectEncodingParserTest, MarkovAutomatonParsing) {
std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::parser::DirectEncodingParser<double>::parseModel(STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.drn");
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> ma = modelPtr->as<storm::models::sparse::MarkovAutomaton<double>>();
// Test if parsed correctly.
ASSERT_EQ(storm::models::ModelType::MarkovAutomaton, modelPtr->getType());
ASSERT_EQ(17ul, ma->getNumberOfStates());
ASSERT_EQ(25ul, ma->getNumberOfTransitions());
ASSERT_EQ(19ul, ma->getNumberOfChoices());
ASSERT_EQ(10ul, ma->getMarkovianStates().getNumberOfSetBits());
ASSERT_EQ(5, ma->getMaximalExitRate());
ASSERT_TRUE(ma->hasRewardModel("avg_waiting_time"));
ASSERT_TRUE(modelPtr->hasLabel("init"));
ASSERT_EQ(1ul, modelPtr->getInitialStates().getNumberOfSetBits());
ASSERT_TRUE(modelPtr->hasLabel("one_job_finished"));
ASSERT_EQ(6ul, modelPtr->getStates("one_job_finished").getNumberOfSetBits());
}

4
travis/build_helper.sh

@ -114,10 +114,10 @@ echo Normalized C++ Standard library location: $(readlink -f $(echo '#include <v
case "$CONFIG" in
DefaultDebug*)
CMAKE_ARGS=(-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DCMAKE_CXX_FLAGS="$STLARG")
CMAKE_ARGS=(-DCMAKE_BUILD_TYPE=Debug -DSTORM_DEVELOPER=ON -DSTORM_PORTABLE=ON -DCMAKE_CXX_FLAGS="$STLARG")
;;
DefaultRelease*)
CMAKE_ARGS=(-DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DCMAKE_CXX_FLAGS="$STLARG")
CMAKE_ARGS=(-DCMAKE_BUILD_TYPE=Release -DSTORM_DEVELOPER=OFF -DSTORM_PORTABLE=ON -DCMAKE_CXX_FLAGS="$STLARG")
;;
*)
echo "Unrecognized value of CONFIG: $CONFIG"; exit 1

Loading…
Cancel
Save