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

made tests work again 

Former-commit-id: bd3e831b0d [formerly cef4348674]
Former-commit-id: 8fd0b70c1e
tempestpy_adaptions
dehnert 8 years ago
parent
8a8aca0062
commit
c2cab571f5
8 changed files with 157 additions and 155 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/cli/cli.cpp
  2. 23
      src/storage/SymbolicModelDescription.cpp
  3. 7
      src/storage/SymbolicModelDescription.h
  4. 17
      src/storage/prism/ToJaniConverter.cpp
  5. 239
      test/functional/builder/DdJaniModelBuilderTest.cpp
  6. 14
      test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
  7. 4
      test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp
  8. 6
      test/functional/utility/ModelInstantiatorTest.cpp

2
src/cli/cli.cpp
View File

@ -219,7 +219,7 @@ namespace storm {
// Get the string that assigns values to the unknown currently undefined constants in the model.
std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
model.preprocess(constantDefinitionString);
model = model.preprocess(constantDefinitionString);
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;

23
src/storage/SymbolicModelDescription.cpp
View File

@ -17,6 +17,14 @@ namespace storm {
// Intentionally left empty.
}
SymbolicModelDescription& SymbolicModelDescription::operator=(storm::jani::Model const& model) {
this->modelDescription = model;
}
SymbolicModelDescription& SymbolicModelDescription::operator=(storm::prism::Program const& program) {
this->modelDescription = program;
}
bool SymbolicModelDescription::hasModel() const {
return static_cast<bool>(modelDescription);
}
@ -47,27 +55,26 @@ namespace storm {
return boost::get<storm::prism::Program>(modelDescription.get());
}
void SymbolicModelDescription::toJani(bool makeVariablesGlobal) {
SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const {
if (this->isJaniModel()) {
return;
return *this;
}
if (this->isPrismProgram()) {
modelDescription = this->asPrismProgram().toJani(makeVariablesGlobal);
return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
}
}
void SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) {
SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
if (this->isJaniModel()) {
std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString);
this->modelDescription = this->asJaniModel().defineUndefinedConstants(substitution);
this->modelDescription = this->asJaniModel().substituteConstants();
return SymbolicModelDescription(this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants());
} else if (this->isPrismProgram()) {
std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString);
this->modelDescription = this->asPrismProgram().defineUndefinedConstants(substitution);
this->modelDescription = this->asPrismProgram().substituteConstants();
return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(substitution).substituteConstants());
}
return *this;
}
}

7
src/storage/SymbolicModelDescription.h
View File

@ -14,6 +14,9 @@ namespace storm {
SymbolicModelDescription(storm::jani::Model const& model);
SymbolicModelDescription(storm::prism::Program const& program);
SymbolicModelDescription& operator=(storm::jani::Model const& model);
SymbolicModelDescription& operator=(storm::prism::Program const& program);
bool hasModel() const;
bool isJaniModel() const;
bool isPrismProgram() const;
@ -24,9 +27,9 @@ namespace storm {
storm::jani::Model const& asJaniModel() const;
storm::prism::Program const& asPrismProgram() const;
void toJani(bool makeVariablesGlobal = true);
SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const;
void preprocess(std::string const& constantDefinitionString = "");
SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
private:
boost::optional<boost::variant<storm::jani::Model, storm::prism::Program>> modelDescription;

17
src/storage/prism/ToJaniConverter.cpp
View File

@ -137,11 +137,15 @@ namespace storm {
}
STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented.");
}
STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition.");
// Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
// previously built mapping to make variables global that are read by more than one module.
bool firstModule = true;
for (auto const& module : program.getModules()) {
// Keep track of the action indices contained in this module.
std::set<uint_fast64_t> actionIndicesOfModule;
storm::jani::Automaton automaton(module.getName());
for (auto const& variable : module.getIntegerVariables()) {
storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression());
@ -184,6 +188,8 @@ namespace storm {
}
for (auto const& command : module.getCommands()) {
actionIndicesOfModule.insert(command.getActionIndex());
boost::optional<storm::expressions::Expression> rateExpression;
std::vector<storm::jani::EdgeDestination> destinations;
if (program.getModelType() == Program::ModelType::CTMC || program.getModelType() == Program::ModelType::CTMDP) {
@ -224,6 +230,17 @@ namespace storm {
automaton.addEdge(newEdge);
}
// Now remove for all actions of this module the corresponding transient assignments, because we must
// not deal out this reward multiple times.
// NOTE: This only works for the standard composition and not for any custom compositions. This case
// must be checked for earlier.
for (auto actionIndex : actionIndicesOfModule) {
auto it = transientEdgeAssignments.find(actionIndex);
if (it != transientEdgeAssignments.end()) {
transientEdgeAssignments.erase(it);
}
}
janiModel.addAutomaton(automaton);
firstModule = false;
}

239
test/functional/builder/DdJaniModelBuilderTest.cpp
View File

@ -6,6 +6,7 @@
#include "src/storage/dd/Add.h"
#include "src/storage/dd/Bdd.h"
#include "src/storage/SymbolicModelDescription.h"
#include "src/models/symbolic/StandardRewardModel.h"
#include "src/parser/PrismParser.h"
@ -16,78 +17,70 @@
#include "src/settings/modules/IOSettings.h"
TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::jani::Model janiModel = program.toJani(true);
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
janiModel = program.toJani(true);
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
model = builder.build(janiModel);
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
TEST(DdJaniModelBuilderTest_Cudd, Dtmc) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::jani::Model janiModel = program.toJani(true);
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(677ul, model->getNumberOfStates());
EXPECT_EQ(867ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(8607ul, model->getNumberOfStates());
EXPECT_EQ(15113ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(1728ul, model->getNumberOfStates());
EXPECT_EQ(2505ul, model->getNumberOfTransitions());
}
@ -96,38 +89,34 @@ TEST(DdJaniModelBuilderTest_Sylvan, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build();
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
@ -136,47 +125,43 @@ TEST(DdJaniModelBuilderTest_Cudd, Ctmc) {
// Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build();
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
EXPECT_EQ(276ul, model->getNumberOfStates());
EXPECT_EQ(1120ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(3478ul, model->getNumberOfStates());
EXPECT_EQ(14639ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(12ul, model->getNumberOfStates());
EXPECT_EQ(22ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(810ul, model->getNumberOfStates());
EXPECT_EQ(3699ul, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_EQ(66ul, model->getNumberOfStates());
EXPECT_EQ(189ul, model->getNumberOfTransitions());
}
TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build();
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@ -185,10 +170,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@ -197,10 +181,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@ -209,10 +192,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@ -221,10 +203,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@ -233,10 +214,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::Sylvan, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
@ -247,10 +227,10 @@ TEST(DdJaniModelBuilderTest_Sylvan, Mdp) {
}
TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build();
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@ -259,10 +239,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(436ul, mdp->getNumberOfTransitions());
EXPECT_EQ(254ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@ -271,10 +250,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(654ul, mdp->getNumberOfTransitions());
EXPECT_EQ(573ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@ -283,10 +261,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(492ul, mdp->getNumberOfTransitions());
EXPECT_EQ(400ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@ -295,10 +272,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(1282ul, mdp->getNumberOfTransitions());
EXPECT_EQ(1054ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@ -307,10 +283,9 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
EXPECT_EQ(5585ul, mdp->getNumberOfTransitions());
EXPECT_EQ(5519ul, mdp->getNumberOfChoices());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
janiModel = program.toJani(true);
builder = storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double>(janiModel);
model = builder.build();
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
model = builder.build(janiModel);
EXPECT_TRUE(model->getType() == storm::models::ModelType::Mdp);
mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD>>();
@ -321,8 +296,8 @@ TEST(DdJaniModelBuilderTest_Cudd, Mdp) {
}
TEST(DdJaniModelBuilderTest_Cudd, IllegalSynchronizingWrites) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::jani::Model janiModel = program.toJani(true);
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder(janiModel);
EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(), storm::exceptions::WrongFormatException);
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
storm::builder::DdJaniModelBuilder<storm::dd::DdType::CUDD, double> builder;
EXPECT_THROW(std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = builder.build(janiModel), storm::exceptions::WrongFormatException);
}

14
test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp
View File

@ -24,7 +24,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) {
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@ -95,7 +95,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@ -189,7 +189,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) {
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@ -233,7 +233,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) {
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@ -297,7 +297,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@ -389,7 +389,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@ -455,7 +455,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) {
storm::prism::Program program = storm::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, constantsAsString);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);;
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);;
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());

4
test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp
View File

@ -23,7 +23,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) {
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaFile, program);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaFile, program);
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
@ -91,7 +91,7 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) {
carl::VariablePool::getInstance().clear();
storm::prism::Program program = storm::parseProgram(programFile);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
std::shared_ptr<storm::models::sparse::Mdp<storm::RationalFunction>> model = storm::buildSparseModel<storm::RationalFunction>(program, formulas)->as<storm::models::sparse::Mdp<storm::RationalFunction>>();
auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());

6
test/functional/utility/ModelInstantiatorTest.cpp
View File

@ -26,7 +26,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
program.checkValidity();
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
ASSERT_TRUE(formulas.size()==1);
// Parametric model
storm::generator::NextStateGeneratorOptions options(*formulas.front());
@ -144,7 +144,7 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
program.checkValidity();
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
ASSERT_TRUE(formulas.size()==1);
// Parametric model
storm::generator::NextStateGeneratorOptions options(*formulas.front());
@ -214,7 +214,7 @@ TEST(ModelInstantiatorTest, Consensus) {
// Program and formula
storm::prism::Program program = storm::parseProgram(programFile);
program.checkValidity();
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForProgram(formulaAsString, program);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForPrismProgram(formulaAsString, program);
ASSERT_TRUE(formulas.size()==1);
// Parametric model
storm::generator::NextStateGeneratorOptions options(*formulas.front());

Write Preview
Loading…
Cancel
Save