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

Fixed issues with the refactored parser interface and move semantics 

Former-commit-id: e92111749e
tempestpy_adaptions
PBerger 12 years ago
parent
8a8a0c1ce8
commit
5be52118ba
2 changed files with 8 additions and 10 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm.cpp
  2. 12
      test/performance/graph/GraphTest.cpp

6
src/storm.cpp
View File

@ -241,8 +241,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
storm::settings::Settings* s = storm::settings::instance(); storm::settings::Settings* s = storm::settings::instance();
if (s->isSet("prctl")) { if (s->isSet("prctl")) {
LOG4CPLUS_INFO(logger, "Parsing prctl file: " << s->getString("prctl") << "."); LOG4CPLUS_INFO(logger, "Parsing prctl file: " << s->getString("prctl") << ".");
storm::parser::PrctlFileParser fileParser;
std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = fileParser.parseFormulas(s->getString("prctl"));
std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = storm::parser::PrctlFileParser(s->getString("prctl"));
for (auto formula : formulaList) { for (auto formula : formulaList) {
modelchecker.check(*formula); modelchecker.check(*formula);
@ -317,8 +316,7 @@ int main(const int argc, const char* argv[]) {
} }
} else if (s->isSet("symbolic")) { } else if (s->isSet("symbolic")) {
std::string arg = s->getString("symbolic"); std::string arg = s->getString("symbolic");
storm::parser::PrismParser parser;
storm::adapters::ExplicitModelAdapter adapter(parser.parseFile(arg));
storm::adapters::ExplicitModelAdapter adapter(storm::parser::PrismParserFromFile(arg));
std::shared_ptr<storm::models::AbstractModel<double>> model = adapter.getModel(); std::shared_ptr<storm::models::AbstractModel<double>> model = adapter.getModel();
model->printModelInformationToStream(std::cout); model->printModelInformationToStream(std::cout);
} }

12
test/performance/graph/GraphTest.cpp
View File

@ -104,13 +104,13 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>(); std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8..."); LOG4CPLUS_WARN(logger, "Computing SCC decomposition of synchronous_leader/leader6_8...");
sccDecomposition = storm::utility::graph::performSccDecomposition(*dtmc2);
sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*dtmc2));
LOG4CPLUS_WARN(logger, "Done."); LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 1279673u); ASSERT_EQ(sccDecomposition.size(), 1279673u);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8..."); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of synchronous_leader/leader6_8...");
sccDependencyGraph = dtmc2->extractPartitionDependencyGraph(sccDecomposition);
sccDependencyGraph = std::move(dtmc2->extractPartitionDependencyGraph(sccDecomposition));
LOG4CPLUS_WARN(logger, "Done."); LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 1535367u);
@ -121,13 +121,13 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
std::shared_ptr<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> mdp = parser3.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6..."); LOG4CPLUS_WARN(logger, "Computing SCC decomposition of asynchronous_leader/leader6...");
sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp);
sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*mdp));
LOG4CPLUS_WARN(logger, "Done."); LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 214675); ASSERT_EQ(sccDecomposition.size(), 214675);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6..."); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of asynchronous_leader/leader6...");
sccDependencyGraph = mdp->extractPartitionDependencyGraph(sccDecomposition);
sccDependencyGraph = std::move(mdp->extractPartitionDependencyGraph(sccDecomposition));
LOG4CPLUS_WARN(logger, "Done."); LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 684093u);
@ -138,13 +138,13 @@ TEST(GraphTest, PerformSCCDecompositionAndGetDependencyGraph) {
std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser4.getModel<storm::models::Mdp<double>>();
LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6..."); LOG4CPLUS_WARN(logger, "Computing SCC decomposition of consensus/coin4_6...");
sccDecomposition = storm::utility::graph::performSccDecomposition(*mdp2);
sccDecomposition = std::move(storm::utility::graph::performSccDecomposition(*mdp2));
LOG4CPLUS_WARN(logger, "Done."); LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDecomposition.size(), 63611u); ASSERT_EQ(sccDecomposition.size(), 63611u);
LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6..."); LOG4CPLUS_WARN(logger, "Extracting SCC dependency graph of consensus/coin4_6...");
sccDependencyGraph = mdp2->extractPartitionDependencyGraph(sccDecomposition);
sccDependencyGraph = std::move(mdp2->extractPartitionDependencyGraph(sccDecomposition));
LOG4CPLUS_WARN(logger, "Done."); LOG4CPLUS_WARN(logger, "Done.");
ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u); ASSERT_EQ(sccDependencyGraph.getNonZeroEntryCount(), 213400u);

Write Preview
Loading…
Cancel
Save