Browse Source

fixed two issues: missing include in ToRationalNumberVisitor and missing check for whether actions are reused in a JANI parallel composition

tempestpy_adaptions
dehnert 8 years ago
parent
commit
9c581bd635
  1. 2
      src/storm/storage/expressions/ToRationalNumberVisitor.h
  2. 2
      src/storm/storage/jani/Model.cpp
  3. 6
      src/storm/storage/jani/ParallelComposition.cpp
  4. 10
      src/test/builder/DdJaniModelBuilderTest.cpp

2
src/storm/storage/expressions/ToRationalNumberVisitor.h

@ -2,6 +2,8 @@
#include <unordered_map>
#include <boost/optional.hpp>
#include "storm/adapters/CarlAdapter.h"
#include "storm/storage/expressions/Expression.h"

2
src/storm/storage/jani/Model.cpp

@ -1134,7 +1134,7 @@ namespace storm {
}
bool Model::reusesActionsInComposition() const {
if(composition->isParallelComposition()) {
if (composition->isParallelComposition()) {
return composition->asParallelComposition().areActionsReused();
}
return false;

6
src/storm/storage/jani/ParallelComposition.cpp

@ -195,13 +195,15 @@ namespace storm {
for (auto const& vector : synchronizationVectors) {
std::string const& action = vector.getInput(inputIndex);
if (action != SynchronizationVector::NO_ACTION_INPUT) {
return true;
if (actions.find(action) != actions.end()) {
return true;
}
actions.insert(action);
}
}
// And check recursively, in case we have nested parallel composition
if (subcompositions.at(inputIndex)->isParallelComposition()) {
if(subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) {
if (subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) {
return true;
}
}

10
src/test/builder/DdJaniModelBuilderTest.cpp

@ -17,6 +17,8 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/exceptions/InvalidSettingsException.h"
TEST(DdJaniModelBuilderTest_Sylvan, Dtmc) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel();
@ -363,7 +365,9 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
inputVector.push_back("c");
inputVector.push_back("b");
synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
EXPECT_THROW(newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException);
newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
janiModel.setSystemComposition(newComposition);
EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
}
TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
@ -419,7 +423,9 @@ TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) {
inputVector.push_back("c");
inputVector.push_back("b");
synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
EXPECT_THROW(newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException);
newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
janiModel.setSystemComposition(newComposition);
EXPECT_THROW(model = builder.build(janiModel), storm::exceptions::InvalidSettingsException);
}
TEST(DdJaniModelBuilderTest_Sylvan, Composition) {

Loading…
Cancel
Save