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

added quite some debug output to see where things are going wrong 

Former-commit-id: 4f61d66074 [formerly e11d6fb2b0]
Former-commit-id: d72214ef96
tempestpy_adaptions
dehnert 8 years ago
parent
675b7bb207
commit
3504d09500
8 changed files with 102 additions and 16 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. 22
      src/builder/DdJaniModelBuilder.cpp
  2. 2
      src/builder/DdPrismModelBuilder.cpp
  3. 4
      src/storage/jani/CompositionActionInformationVisitor.cpp
  4. 2
      src/storage/jani/CompositionActionInformationVisitor.h
  5. 3
      src/storage/jani/ParallelComposition.cpp
  6. 7
      src/storage/jani/RenameComposition.cpp
  7. 27
      src/storage/prism/CompositionToJaniVisitor.cpp
  8. 51
      test/functional/builder/DdJaniModelBuilderTest.cpp

22
src/builder/DdJaniModelBuilder.cpp
View File

@ -211,7 +211,7 @@ namespace storm {
}
boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
boost::any_cast<std::set<std::string>>(composition.getSubcomposition().accept(*this, boost::none));
composition.getSubcomposition().accept(*this, data);
return boost::none;
}
@ -322,7 +322,7 @@ namespace storm {
int_fast64_t high = variable.getUpperBound().evaluateAsInt();
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable(variable.getName(), low, high);
STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << "] and " << variablePair.second.getName() << ".");
STORM_LOG_TRACE("Created meta variables for global integer variable: " << variablePair.first.getName() << " and " << variablePair.second.getName() << ".");
result.rowMetaVariables.insert(variablePair.first);
result.variableToRowMetaVariableMap->emplace(variable.getExpressionVariable(), variablePair.first);
@ -1133,6 +1133,7 @@ namespace storm {
subautomata.push_back(boost::any_cast<AutomatonDd>(composition.getSubcomposition(subcompositionIndex).accept(*this, newSynchronizingActionToOffsetMap)));
}
std::cout << "composing " << composition << std::endl;
return composeInParallel(subautomata, composition.getSynchronizationVectors());
}
@ -1211,6 +1212,7 @@ namespace storm {
// Extend all other non-synchronizing actions with the identity of the current subautomaton.
for (auto& actions : nonSynchronizingActions) {
for (auto& action : actions.second) {
STORM_LOG_TRACE("Extending action '" << actionInformation.getActionName(actions.first) << "' with identity of next composition.");
action.transitions *= subautomaton.identity;
}
}
@ -1219,6 +1221,7 @@ namespace storm {
// add it to the overall non-synchronizing action result.
for (auto const& action : subautomaton.actionIndexToAction) {
if (actionsInSynch.find(action.first) == actionsInSynch.end()) {
STORM_LOG_TRACE("Adding action " << actionInformation.getActionName(action.first) << " to non-synchronizing actions and multiply it with system identity.");
nonSynchronizingActions[action.first].push_back(action.second.multiplyTransitions(result.identity));
}
}
@ -1253,6 +1256,10 @@ namespace storm {
}
}
for (auto act : result.actionIndexToAction) {
act.second.transitions.exportToDot("act__" + actionInformation.getActionName(act.first) + ".dot");
}
return result;
}
@ -1505,7 +1512,7 @@ namespace storm {
guard |= edge.guard.toBdd();
transitions += edge.transitions;
joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment);
variableToWritingFragment = joinVariableWritingFragmentMaps(variableToWritingFragment, edge.variableToWritingFragment);
joinTransientAssignmentMaps(transientEdgeAssignments, edge.transientEdgeAssignments);
}
@ -1846,6 +1853,7 @@ namespace storm {
}
ActionDd actionDd = buildActionDdForActionIndex(automaton, actionIndex, actionIndexToLocalNondeterminismVariableOffset.at(actionIndex));
result.actionIndexToAction[actionIndex] = actionDd;
actionDd.transitions.exportToDot("build_" + action.getName() + ".dot");
result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable()));
result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable()));
}
@ -1895,6 +1903,7 @@ namespace storm {
// Add missing global variable identities, action and nondeterminism encodings.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
for (auto& action : automaton.actionIndexToAction) {
action.second.transitions.exportToDot("build_from_aut_" + std::to_string(action.first) + ".dot");
illegalFragment |= action.second.illegalFragment;
addMissingGlobalVariableIdentities(action.second);
storm::dd::Add<Type, ValueType> actionEncoding = encodeAction(action.first != this->model.getSilentActionIndex() ? boost::optional<uint64_t>(action.first) : boost::none, this->variables);
@ -1906,6 +1915,7 @@ namespace storm {
}
result += extendedTransitions;
result.exportToDot("result_after_" + actionInformation.getActionName(action.first) + ".dot");
}
return ComposerResult<Type, ValueType>(result, automaton.transientLocationAssignments, transientEdgeAssignments, illegalFragment, numberOfUsedNondeterminismVariables);
@ -1940,6 +1950,7 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
if (modelType == storm::jani::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::CTMC) {
@ -2141,7 +2152,7 @@ namespace storm {
// Determine the actions that will appear in the parallel composition.
storm::jani::CompositionActionInformationVisitor actionInformationVisitor(model);
storm::jani::ActionInformation actionInformation = actionInformationVisitor.getActionInformation();
storm::jani::ActionInformation actionInformation = actionInformationVisitor.getActionInformation(model.getSystemComposition());
// Create all necessary variables.
CompositionVariableCreator<Type, ValueType> variableCreator(model, actionInformation);
@ -2168,10 +2179,13 @@ namespace storm {
// Perform reachability analysis to obtain reachable states.
storm::dd::Bdd<Type> transitionMatrixBdd = system.transitions.notZero();
system.transitions.exportToDot("trans.dot");
transitionMatrixBdd.template toAdd<ValueType>().exportToDot("transbdd.dot");
if (model.getModelType() == storm::jani::ModelType::MDP) {
transitionMatrixBdd = transitionMatrixBdd.existsAbstract(variables.allNondeterminismVariables);
}
modelComponents.reachableStates = storm::utility::dd::computeReachableStates(modelComponents.initialStates, transitionMatrixBdd, variables.rowMetaVariables, variables.columnMetaVariables);
modelComponents.reachableStates.template toAdd<ValueType>().exportToDot("reach_jani.dot");
// Check that the reachable fragment does not overlap with the illegal fragment.
storm::dd::Bdd<Type> reachableIllegalFragment = modelComponents.reachableStates && system.illegalFragment;

2
src/builder/DdPrismModelBuilder.cpp
View File

@ -1393,6 +1393,8 @@ namespace storm {
labelToExpressionMapping.emplace(label.getName(), label.getStatePredicateExpression());
}
reachableStates.template toAdd<ValueType>().exportToDot("prism_jani.dot");
if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(generationInfo.manager, reachableStates, initialStates, deadlockStates, transitionMatrix, generationInfo.rowMetaVariables, generationInfo.rowExpressionAdapter, generationInfo.columnMetaVariables, generationInfo.columnExpressionAdapter, generationInfo.rowColumnMetaVariablePairs, labelToExpressionMapping, rewardModels));
} else if (program.getModelType() == storm::prism::Program::ModelType::CTMC) {

4
src/storage/jani/CompositionActionInformationVisitor.cpp
View File

@ -30,7 +30,7 @@ namespace storm {
// Intentionally left empty.
}
ActionInformation CompositionActionInformationVisitor::getActionInformation() {
ActionInformation CompositionActionInformationVisitor::getActionInformation(storm::jani::Composition const& composition) {
indexToNameMap.clear();
nameToIndexMap.clear();
@ -45,7 +45,7 @@ namespace storm {
}
++nextFreeActionIndex;
std::set<uint64_t> nonSilentActionIndices = boost::any_cast<std::set<uint64_t>>(model.getSystemComposition().accept(*this, boost::none));
std::set<uint64_t> nonSilentActionIndices = boost::any_cast<std::set<uint64_t>>(composition.accept(*this, boost::none));
return ActionInformation(nonSilentActionIndices, indexToNameMap, nameToIndexMap);
}

2
src/storage/jani/CompositionActionInformationVisitor.h
View File

@ -30,7 +30,7 @@ namespace storm {
public:
CompositionActionInformationVisitor(storm::jani::Model const& model);
ActionInformation getActionInformation();
ActionInformation getActionInformation(storm::jani::Composition const& composition);
virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override;
virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override;

3
src/storage/jani/ParallelComposition.cpp
View File

@ -48,6 +48,7 @@ namespace storm {
stream << ", ";
}
stream << element;
first = false;
}
stream << ") -> " << synchronizationVector.getOutput();
return stream;
@ -130,9 +131,9 @@ namespace storm {
for (auto const& subcomposition : subcompositions) {
if (!first) {
stream << " || ";
first = false;
}
stream << *subcomposition;
first = false;
}
stream << ")[" << boost::algorithm::join(synchronizationVectorsAsStrings, ", ") << "]";
}

7
src/storage/jani/RenameComposition.cpp
View File

@ -35,11 +35,14 @@ namespace storm {
} else {
stream << "tau";
}
renamingStrings.push_back(stream.str());
}
stream << "(" << subcomposition << ") / {" << boost::join(renamingStrings, ", ") << "}";
stream << "(";
subcomposition->write(stream);
stream << ")/{" << boost::join(renamingStrings, ", ") << "} ";
}
}
}
}

27
src/storage/prism/CompositionToJaniVisitor.cpp
View File

@ -2,13 +2,16 @@
#include "src/storage/prism/Compositions.h"
#include "src/storage/jani/Compositions.h"
#include "src/storage/jani/CompositionActionInformationVisitor.h"
#include "src/storage/jani/Model.h"
namespace storm {
namespace prism {
std::shared_ptr<storm::jani::Composition> CompositionToJaniVisitor::toJani(Composition const& composition, storm::jani::Model const& model) {
return boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.accept(*this, model));
auto result = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.accept(*this, model));
std::cout << "got composition " << *result << std::endl;
return result;
}
boost::any CompositionToJaniVisitor::visit(ModuleComposition const& composition, boost::any const& data) {
@ -41,11 +44,23 @@ namespace storm {
auto rightSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getRightSubcomposition().accept(*this, data));
storm::jani::Model const& model = boost::any_cast<storm::jani::Model const&>(data);
std::set<std::string> allActions;
for (auto const& action : model.getActions()) {
allActions.insert(action.getName());
storm::jani::CompositionActionInformationVisitor visitor(model);
storm::jani::ActionInformation leftActionInformation = visitor.getActionInformation(*leftSubcomposition);
storm::jani::ActionInformation rightActionInformation = visitor.getActionInformation(*rightSubcomposition);
std::set<std::string> leftActions;
for (auto const& actionIndex : leftActionInformation.getNonSilentActionIndices()) {
leftActions.insert(leftActionInformation.getActionName(actionIndex));
}
std::set<std::string> rightActions;
for (auto const& actionIndex : rightActionInformation.getNonSilentActionIndices()) {
rightActions.insert(rightActionInformation.getActionName(actionIndex));
}
std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(leftSubcomposition, rightSubcomposition, allActions);
std::set<std::string> commonActions;
std::set_intersection(leftActions.begin(), leftActions.end(), rightActions.begin(), rightActions.end(), std::inserter(commonActions, commonActions.begin()));
std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(leftSubcomposition, rightSubcomposition, commonActions);
return result;
}
@ -63,4 +78,4 @@ namespace storm {
return result;
}
}
}
}

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

@ -365,3 +365,54 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e"));
EXPECT_THROW(newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException);
}
TEST(DdJaniModelBuilderTest_Sylvan, Composition) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.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>>();
EXPECT_EQ(21ul, mdp->getNumberOfStates());
EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
EXPECT_EQ(61ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.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>>();
EXPECT_EQ(8ul, mdp->getNumberOfStates());
EXPECT_EQ(21ul, mdp->getNumberOfTransitions());
EXPECT_EQ(21ul, mdp->getNumberOfChoices());
}
TEST(DdJaniModelBuilderTest_Cudd, Composition) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.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>>();
EXPECT_EQ(21ul, mdp->getNumberOfStates());
EXPECT_EQ(61ul, mdp->getNumberOfTransitions());
EXPECT_EQ(61ul, mdp->getNumberOfChoices());
modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition2.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>>();
EXPECT_EQ(8ul, mdp->getNumberOfStates());
EXPECT_EQ(21ul, mdp->getNumberOfTransitions());
EXPECT_EQ(21ul, mdp->getNumberOfChoices());
}
Write Preview
Loading…
Cancel
Save