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

Intermediate commit. 

Former-commit-id: e5f251718f
main
dehnert 10 years ago
parent
0f0baf61a4
commit
8c1870eb54
23 changed files with 904 additions and 56 deletions
Split View
  1. 175
      src/builder/DdPrismModelBuilder.cpp
  2. 16
      src/builder/DdPrismModelBuilder.h
  3. 6
      src/builder/ExplicitPrismModelBuilder.cpp
  4. 2
      src/parser/PrismParser.cpp
  5. 7
      src/storage/expressions/Expression.cpp
  6. 8
      src/storage/expressions/Expression.h
  7. 15
      src/storage/prism/Command.cpp
  8. 9
      src/storage/prism/Command.h
  9. 25
      src/storage/prism/Module.cpp
  10. 8
      src/storage/prism/Module.h
  11. 84
      src/storage/prism/Program.cpp
  12. 20
      src/storage/prism/Program.h
  13. 14
      src/storage/prism/RewardModel.cpp
  14. 9
      src/storage/prism/RewardModel.h
  15. 3
      src/utility/cli.h
  16. 27
      test/functional/builder/DdPrismModelBuilderTest.cpp
  17. 28
      test/functional/builder/ExplicitPrismModelBuilderTest.cpp
  18. 60
      test/functional/builder/coin2-2.nm
  19. 130
      test/functional/builder/csma2-2.nm
  20. 170
      test/functional/builder/firewire3-0.5.nm
  21. 91
      test/functional/builder/leader3.nm
  22. 40
      test/functional/builder/two_dice.nm
  23. 13
      wlan0_collide.nm

175
src/builder/DdPrismModelBuilder.cpp
View File

@ -82,23 +82,25 @@ namespace storm {
updateDd *= result;
}
// FIXME: global boolean variables cause problems. They cannot be added here, because then synchronization goes wrong.
// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalBooleanVariables().size(); ++i) {
// storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(i);
// if (update.getAssignmentMapping().find(booleanVariable.getName()) == update.getAssignmentMapping().end()) {
// // Multiply identity matrix
// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(booleanVariable.getName());
// }
// }
//
// // All unused global integer variables do not change
// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalIntegerVariables().size(); ++i) {
// storm::prism::IntegerVariable const& integerVariable = generationInfo.program.getGlobalIntegerVariables().at(i);
// if (update.getAssignmentMapping().find(integerVariable.getName()) == update.getAssignmentMapping().end()) {
// // Multiply identity matrix
// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName());
// }
// }
// This works under the assumption that global variables are only written in non-synchronzing commands, but
// is not checked here.
for (auto const& booleanVariable : generationInfo.program.getGlobalBooleanVariables()) {
storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(booleanVariable.getExpressionVariable());
if (assignedVariables.find(metaVariable) == assignedVariables.end()) {
STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName());
updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable());
}
}
// All unused global integer variables do not change
for (auto const& integerVariable : generationInfo.program.getGlobalIntegerVariables()) {
storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(integerVariable.getExpressionVariable());
if (assignedVariables.find(metaVariable) == assignedVariables.end()) {
STORM_LOG_TRACE("Multiplying identity of variable " << integerVariable.getName());
updateDd *= generationInfo.variableToIdentityMap.at(integerVariable.getExpressionVariable());
}
}
// All unassigned boolean variables need to keep their value.
for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
@ -140,6 +142,7 @@ namespace storm {
commandDd += updateDd;
}
(guardDd * commandDd).exportToDot(module.getName() + "_" + command.getActionName() + ".dot");
return ActionDecisionDiagram(guardDd, guardDd * commandDd);
} else {
return ActionDecisionDiagram(*generationInfo.manager);
@ -152,16 +155,28 @@ namespace storm {
for (storm::prism::Command const& command : module.getCommands()) {
// Determine whether the command is relevant for the selected action.
bool relevant = (!synchronizationActionIndex && !command.isLabeled()) || (synchronizationActionIndex && command.getActionIndex() == synchronizationActionIndex.get());
bool relevant = (!synchronizationActionIndex && !command.isLabeled()) || (synchronizationActionIndex && command.isLabeled() && command.getActionIndex() == synchronizationActionIndex.get());
if (!relevant) {
continue;
}
if (synchronizationActionIndex) {
std::cout << command << " is relevant for synch " << synchronizationActionIndex.get() << std::endl;
}
// At this point, the command is known to be relevant for the action.
commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command));
}
if (synchronizationActionIndex && synchronizationActionIndex.get() == 0) {
int i = 0;
for (auto const& commandDd : commandDds) {
commandDd.transitionsDd.exportToDot("cmd_" + std::to_string(i) + ".dot");
++i;
}
}
ActionDecisionDiagram result(*generationInfo.manager);
if (!commandDds.empty()) {
switch (generationInfo.program.getModelType()){
@ -318,6 +333,9 @@ namespace storm {
storm::dd::Dd<Type> action1Extended = action1.transitionsDd * identityDd2;
storm::dd::Dd<Type> action2Extended = action2.transitionsDd * identityDd1;
action1.transitionsDd.exportToDot("act1.dot");
action2.transitionsDd.exportToDot("act2.dot");
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, 0);
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
@ -329,24 +347,28 @@ namespace storm {
// Bring both choices to the same number of variables that encode the nondeterminism.
uint_fast64_t numberOfUsedNondeterminismVariables = std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables);
std::cout << "max used nondet: " << numberOfUsedNondeterminismVariables << std::endl;
if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) {
storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables + 1; i <= action1.numberOfUsedNondeterminismVariables; ++i) {
for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) {
nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
}
action2Extended *= nondeterminisimEncoding;
} else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) {
storm::dd::Dd<Type> nondeterminisimEncoding = generationInfo.manager->getOne();
for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables + 1; i <= action2.numberOfUsedNondeterminismVariables; ++i) {
for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) {
nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
}
action1Extended *= nondeterminisimEncoding;
}
action1Extended.exportToDot("act1ext.dot");
action2Extended.exportToDot("act2ext.dot");
// Add a new variable that resolves the nondeterminism between the two choices.
storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables + 1], 1).ite(action2Extended, action1Extended);
storm::dd::Dd<Type> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2Extended, action1Extended);
return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1);
} else {
@ -358,15 +380,18 @@ namespace storm {
typename DdPrismModelBuilder<Type>::ModuleDecisionDiagram DdPrismModelBuilder<Type>::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap) {
// Start by creating the action DD for the independent action.
ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, boost::optional<uint_fast64_t>(), 0);
uint_fast64_t numberOfUsedNondeterminismVariables = independentActionDd.numberOfUsedNondeterminismVariables;
// Create module DD for all synchronizing actions of the module.
std::map<uint_fast64_t, ActionDecisionDiagram> actionIndexToDdMap;
for (auto const& actionIndex : module.getActionIndices()) {
STORM_LOG_TRACE("Creating DD for action '" << actionIndex << "'.");
actionIndexToDdMap.emplace(actionIndex, createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex)));
ActionDecisionDiagram tmp = createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex));
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, tmp.numberOfUsedNondeterminismVariables);
actionIndexToDdMap.emplace(actionIndex, tmp);
}
return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()));
return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName()), numberOfUsedNondeterminismVariables);
}
template <storm::dd::DdType Type>
@ -375,17 +400,15 @@ namespace storm {
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
storm::dd::Dd<Type> result = generationInfo.manager->getZero();
// First, determine the maximal variable index that is used.
uint_fast64_t numberOfUsedNondeterminismVariables = module.independentAction.numberOfUsedNondeterminismVariables;
for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, synchronizingAction.second.numberOfUsedNondeterminismVariables);
}
// First, determine the highest number of nondeterminism variables that is used in any action and make
// all actions use the same amout of nondeterminism variables.
uint_fast64_t numberOfUsedNondeterminismVariables = module.numberOfUsedNondeterminismVariables;
std::cout << "pumping number of used nondet variables to " << numberOfUsedNondeterminismVariables << std::endl;
// Now make all actions use the same amount of nondeterminism variables.
// Add variables to independent action DD.
storm::dd::Dd<Type> nondeterminismEncoding = generationInfo.manager->getOne();
for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables + 1; i <= numberOfUsedNondeterminismVariables; ++i) {
for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
std::cout << "adding " << i << " to independent" << std::endl;
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
}
result = module.independentAction.transitionsDd * nondeterminismEncoding;
@ -394,7 +417,7 @@ namespace storm {
std::map<uint_fast64_t, storm::dd::Dd<Type>> synchronizingActionToDdMap;
for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
nondeterminismEncoding = generationInfo.manager->getOne();
for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables + 1; i <= numberOfUsedNondeterminismVariables; ++i) {
for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables; i < numberOfUsedNondeterminismVariables; ++i) {
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0);
}
synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding);
@ -422,8 +445,9 @@ namespace storm {
}
// Now, we can simply add all synchronizing actions to the result.
for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
result += synchronizingAction.second.transitionsDd;
for (auto const& synchronizingAction : synchronizingActionToDdMap) {
synchronizingAction.second.exportToDot("synch" + std::to_string(synchronizingAction.first) + ".dot");
result += synchronizingAction.second;
}
return result;
@ -466,7 +490,9 @@ namespace storm {
ModuleDecisionDiagram nextModule = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap);
// Combine the non-synchronizing action.
uint_fast64_t numberOfUsedNondeterminismVariables = nextModule.numberOfUsedNondeterminismVariables;
system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, nextModule.independentAction, system.identity, nextModule.identity);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.independentAction.numberOfUsedNondeterminismVariables);
// For all synchronizing actions that the next module does not have, we need to multiply the identity of the next module.
for (auto& action : system.synchronizingActionToDecisionDiagramMap) {
@ -479,13 +505,19 @@ namespace storm {
for (auto const& actionIndex : currentModule.getActionIndices()) {
if (system.hasSynchronizingAction(actionIndex)) {
system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
} else {
system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, ActionDecisionDiagram(*generationInfo.manager), nextModule.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, nextModule.identity);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
}
}
// Combine identity matrices.
system.identity = system.identity * nextModule.identity;
// Keep track of the number of nondeterminism variables used.
std::cout << "num used: " << numberOfUsedNondeterminismVariables << std::endl;
system.numberOfUsedNondeterminismVariables = std::max(system.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables);
}
storm::dd::Dd<Type> result = createSystemFromModule(generationInfo, system);
@ -493,6 +525,15 @@ namespace storm {
// For DTMCs, we normalize each row to 1 (to account for non-determinism).
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
result = result / result.sumAbstract(generationInfo.columnMetaVariables);
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
// For MDPs, we need to throw away the nondeterminism variables from the generation information that
// were never used.
std::cout << "System uses " << system.numberOfUsedNondeterminismVariables << "nd vars" << std::endl;
for (uint_fast64_t index = system.numberOfUsedNondeterminismVariables; index < generationInfo.nondeterminismMetaVariables.size(); ++index) {
std::cout << "removing " << generationInfo.nondeterminismMetaVariables[index].getName() << std::endl;
generationInfo.allNondeterminismVariables.erase(generationInfo.nondeterminismMetaVariables[index]);
}
generationInfo.nondeterminismMetaVariables.resize(system.numberOfUsedNondeterminismVariables);
}
return std::make_pair(result, system);
@ -508,9 +549,24 @@ namespace storm {
preparedProgram = program;
}
preparedProgram = preparedProgram.substituteConstants();
if (preparedProgram.hasUndefinedConstants()) {
std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = preparedProgram.getUndefinedConstants();
std::stringstream stream;
bool printComma = false;
for (auto const& constant : undefinedConstants) {
if (printComma) {
stream << ", ";
} else {
printComma = true;
}
stream << constant.get().getName() << " (" << constant.get().getType() << ")";
}
stream << ".";
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
}
// std::cout << "translated prog: " << preparedProgram << std::endl;
preparedProgram = preparedProgram.substituteConstants();
std::cout << "translated prog: " << preparedProgram << std::endl;
// Start by initializing the structure used for storing all information needed during the model generation.
// In particular, this creates the meta variables used to encode the model.
@ -519,33 +575,55 @@ namespace storm {
auto clock = std::chrono::high_resolution_clock::now();
std::pair<storm::dd::Dd<Type>, ModuleDecisionDiagram> transitionMatrixModulePair = createSystemDecisionDiagram(generationInfo);
storm::dd::Dd<Type> transitionMatrix = transitionMatrixModulePair.first;
transitionMatrix.exportToDot("trans.dot");
ModuleDecisionDiagram const& globalModule = transitionMatrixModulePair.second;
// Cut the transition matrix to the reachable fragment of the state space.
storm::dd::Dd<Type> reachableStates = computeReachableStates(generationInfo, createInitialStatesDecisionDiagram(generationInfo), transitionMatrix);
transitionMatrix *= reachableStates;
reachableStates.exportToDot("reach.dot");
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Dd<Type> statesWithTransition = transitionMatrix.notZero();
if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables);
statesWithTransition = statesWithTransition.existsAbstract(generationInfo.allNondeterminismVariables);
statesWithTransition.exportToDot("after_exists.dot");
}
statesWithTransition = statesWithTransition.existsAbstract(generationInfo.columnMetaVariables);
storm::dd::Dd<Type> deadlockStates = reachableStates * !statesWithTransition;
deadlockStates.exportToDot("deadlocks.dot");
if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now.
if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) {
STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states.");
// FIXME: For MDPs, we need to use an action encoding if we do not want to attach a lot of self-loops.
transitionMatrix += deadlockStates * globalModule.identity;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
}
// if (!deadlockStates.isZero()) {
// // If we need to fix deadlocks, we do so now.
// if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) {
// std::cout << "fixing " << deadlockStates.getNonZeroCount() << std::endl;
// STORM_LOG_WARN("Fixing deadlocks in " << deadlockStates.getNonZeroCount() << " states.");
//
// if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
// // For DTMCs, we can simply add the identity of the global module for all deadlock states.
// transitionMatrix += deadlockStates * globalModule.identity;
// } else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
// // For MDPs, however, we need to select an action associated with the self-loop, if we do not
// // want to attach a lot of self-loops to the deadlock states.
// storm::dd::Dd<Type> action = generationInfo.manager->getOne();
// std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), [&action,&generationInfo] (storm::expressions::Variable const& metaVariable) { action *= !generationInfo.manager->getIdentity(metaVariable); } );
// transitionMatrix += deadlockStates * globalModule.identity * action;
// (deadlockStates * globalModule.identity * action).exportToDot("selfloops.dot");
// }
// } else {
// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The model contains " << deadlockStates.getNonZeroCount() << " deadlock states. Please unset the option to not fix deadlocks, if you want to fix them automatically.");
// }
// } else {
// std::cout << "no deadlocks" << std::endl;
// }
transitionMatrix.exportToDot("trans_reach.dot");
for (auto const& var : transitionMatrix.getContainedMetaVariables()) {
std::cout << "var: " << var.getName() << std::endl;
}
return std::make_pair(reachableStates, transitionMatrix * reachableStates);
std::cout << reachableStates.getNonZeroCount() << " states and " << transitionMatrix.getNonZeroCount() << " transitions." << std::endl;
return std::make_pair(reachableStates, transitionMatrix);
}
template <storm::dd::DdType Type>
@ -569,6 +647,7 @@ namespace storm {
transitionBdd = transitionBdd.existsAbstract(generationInfo.allNondeterminismVariables);
}
transitionBdd.exportToDot("trans01.dot");
// Perform the BFS to discover all reachable states.
bool changed = true;

16
src/builder/DdPrismModelBuilder.h
View File

@ -91,15 +91,15 @@ namespace storm {
// This structure holds all decision diagrams related to a module.
struct ModuleDecisionDiagram {
ModuleDecisionDiagram() : independentAction(), synchronizingActionToDecisionDiagramMap(), identity() {
ModuleDecisionDiagram() : independentAction(), synchronizingActionToDecisionDiagramMap(), identity(), numberOfUsedNondeterminismVariables(0) {
// Intentionally left empty.
}
ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()) {
ModuleDecisionDiagram(storm::dd::DdManager<Type> const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()), numberOfUsedNondeterminismVariables(0) {
// Intentionally left empty.
}
ModuleDecisionDiagram(ActionDecisionDiagram const& independentAction, std::map<uint_fast64_t, ActionDecisionDiagram> const& synchronizingActionToDecisionDiagramMap, storm::dd::Dd<Type> const& identity) : independentAction(independentAction), synchronizingActionToDecisionDiagramMap(synchronizingActionToDecisionDiagramMap), identity(identity) {
ModuleDecisionDiagram(ActionDecisionDiagram const& independentAction, std::map<uint_fast64_t, ActionDecisionDiagram> const& synchronizingActionToDecisionDiagramMap, storm::dd::Dd<Type> const& identity, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : independentAction(independentAction), synchronizingActionToDecisionDiagramMap(synchronizingActionToDecisionDiagramMap), identity(identity), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) {
// Intentionally left empty.
}
@ -118,6 +118,9 @@ namespace storm {
// A decision diagram that represents the identity of this module.
storm::dd::Dd<Type> identity;
// The number of variables encoding the nondeterminism that were actually used.
uint_fast64_t numberOfUsedNondeterminismVariables;
};
/*!
@ -177,8 +180,8 @@ namespace storm {
*/
void createMetaVariablesAndIdentities() {
// Add synchronization variables.
for (uint_fast64_t i = 0; i < program.getActionIndices().size(); ++i) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable("sync" + std::to_string(i));
for (auto const& actionIndex : program.getActionIndices()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(program.getActionName(actionIndex));
synchronizationMetaVariables.push_back(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
@ -209,7 +212,8 @@ namespace storm {
storm::dd::Dd<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
} for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
}
for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
rowMetaVariables.insert(variablePair.first);

6
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -103,6 +103,8 @@ namespace storm {
// If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
#ifdef STORM_HAVE_CARL
// If the program either has undefined constants or we are building a parametric model, but the parameters
// not only appear in the probabilities, we re
if (!std::is_same<ValueType, storm::RationalFunction>::value && preparedProgram.hasUndefinedConstants()) {
#else
if (preparedProgram.hasUndefinedConstants()) {
@ -120,6 +122,10 @@ namespace storm {
}
stream << ".";
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
#ifdef STORM_HAVE_CARL
} else if (std::is_same<ValueType, storm::RationalFunction>::value && !preparedProgram.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
#endif
}
// Now that we have defined all the constants in the program, we need to substitute their appearances in

2
src/parser/PrismParser.cpp
View File

@ -142,7 +142,7 @@ namespace storm {
commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > +(qi::char_ - qi::lit(";")) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_r1)];
commandDefinition.name("command definition");
moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > *commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
moduleDefinition.name("module definition");
moduleRenaming = ((qi::lit("module") >> identifier >> qi::lit("=")) > identifier > qi::lit("[")

7
src/storage/expressions/Expression.cpp
View File

@ -100,6 +100,13 @@ namespace storm {
return result;
}
bool Expression::containsVariable(std::set<storm::expressions::Variable> const& variables) const {
std::set<storm::expressions::Variable> appearingVariables = this->getVariables();
std::set<storm::expressions::Variable> intersection;
std::set_intersection(variables.begin(), variables.end(), appearingVariables.begin(), appearingVariables.end(), std::inserter(intersection, intersection.begin()));
return !intersection.empty();
}
bool Expression::isRelationalExpression() const {
if (!this->isFunctionApplication()) {
return false;

8
src/storage/expressions/Expression.h
View File

@ -213,6 +213,14 @@ namespace storm {
*/
std::set<storm::expressions::Variable> getVariables() const;
/*!
* Retrieves whether the expression contains any of the given variables.
*
* @param variables The variables to search for.
* @return True iff any of the variables appear in the expression.
*/
bool containsVariable(std::set<storm::expressions::Variable> const& variables) const;
/*!
* Retrieves the base expression underlying this expression object. Note that prior to calling this, the
* expression object must be properly initialized.

15
src/storage/prism/Command.cpp
View File

@ -48,6 +48,21 @@ namespace storm {
return labeled;
}
bool Command::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
if (this->getGuardExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
for (auto const& update : this->getUpdates()) {
for (auto const& assignment : update.getAssignments()) {
if (assignment.getExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
}
return true;
}
std::ostream& operator<<(std::ostream& stream, Command const& command) {
stream << "[" << command.getActionName() << "] " << command.getGuardExpression() << " -> ";
for (uint_fast64_t i = 0; i < command.getUpdates().size(); ++i) {

9
src/storage/prism/Command.h
View File

@ -99,6 +99,15 @@ namespace storm {
*/
bool isLabeled() const;
/*!
* Checks whether the given set of variables only appears in the update probabilities of the command.
*
* @param undefinedConstantVariables The set of variables that may only appear in the update probabilities
* of the command.
* @return True iff the given set of variables only appears in the update probabilities of the command.
*/
bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
friend std::ostream& operator<<(std::ostream& stream, Command const& command);
private:

25
src/storage/prism/Module.cpp
View File

@ -170,6 +170,31 @@ namespace storm {
return Module(this->getName(), newBooleanVariables, newIntegerVariables, newCommands, this->getFilename(), this->getLineNumber());
}
bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
for (auto const& booleanVariable : this->getBooleanVariables()) {
if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
for (auto const& integerVariable : this->getIntegerVariables()) {
if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
for (auto const& command : this->getCommands()) {
command.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
}
return true;
}
std::ostream& operator<<(std::ostream& stream, Module const& module) {
stream << "module " << module.getName() << std::endl;
for (auto const& booleanVariable : module.getBooleanVariables()) {

8
src/storage/prism/Module.h
View File

@ -196,6 +196,14 @@ namespace storm {
*/
Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
/*!
* Checks whether the given variables only appear in the update probabilities of the module and nowhere else.
*
* @param undefinedConstantVariables A set of variables that may only appear in the update probabilities.
* @return True iff the given variables only appear in the update probabilities of the module and nowhere else.
*/
bool containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
friend std::ostream& operator<<(std::ostream& stream, Module const& module);
private:

84
src/storage/prism/Program.cpp
View File

@ -11,7 +11,7 @@
namespace storm {
namespace prism {
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, bool fixInitialConstruct, storm::prism::InitialConstruct const& initialConstruct, std::vector<Label> const& labels, std::string const& filename, uint_fast64_t lineNumber, bool checkValidity) : LocatedInformation(filename, lineNumber), manager(manager), modelType(modelType), constants(constants), constantToIndexMap(), globalBooleanVariables(globalBooleanVariables), globalBooleanVariableToIndexMap(), globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), actionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() {
this->createMappings();
// Create a new initial construct if the corresponding flag was set.
@ -53,6 +53,81 @@ namespace storm {
return false;
}
bool Program::hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards() const {
if (!this->hasUndefinedConstants()) {
return true;
}
// Gather the variables of all undefined constants.
std::set<storm::expressions::Variable> undefinedConstantVariables;
for (auto const& constant : this->getConstants()) {
if (!constant.isDefined()) {
undefinedConstantVariables.insert(constant.getExpressionVariable());
}
}
// Now it remains to check that the intersection of the variables used in the program with the undefined
// constants' variables is empty (except for the update probabilities).
// Start by checking the defining expressions of all defined constants.
for (auto const& constant : this->getConstants()) {
if (constant.isDefined()) {
if (constant.getExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
}
// Now check initial value expressions of global variables.
for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
if (integerVariable.getUpperBoundExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
// Then check the formulas.
for (auto const& formula : this->getFormulas()) {
if (formula.getExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
// Proceed by checking each of the modules.
for (auto const& module : this->getModules()) {
module.containsVariablesOnlyInUpdateProbabilities(undefinedConstantVariables);
}
// Check the reward models.
for (auto const& rewardModel : this->getRewardModels()) {
rewardModel.containsVariablesOnlyInRewardValueExpressions(undefinedConstantVariables);
}
// Initial construct.
if (this->getInitialConstruct().getInitialStatesExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
// Labels.
for (auto const& label : this->getLabels()) {
if (label.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
return true;
}
std::vector<std::reference_wrapper<storm::prism::Constant const>> Program::getUndefinedConstants() const {
std::vector<std::reference_wrapper<storm::prism::Constant const>> result;
for (auto const& constant : this->getConstants()) {
@ -150,6 +225,12 @@ namespace storm {
return this->actionIndices;
}
std::string const& Program::getActionName(uint_fast64_t actionIndex) const {
auto const& indexNamePair = this->indexToActionMap.find(actionIndex);
STORM_LOG_THROW(indexNamePair != this->indexToActionMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action index " << actionIndex << ".");
return indexNamePair->second;
}
std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
auto const& nameIndexPair = this->actionToIndexMap.find(action);
STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");
@ -272,6 +353,7 @@ namespace storm {
for (auto const& actionIndexPair : this->getActionNameToIndexMapping()) {
this->actions.insert(actionIndexPair.first);
this->actionIndices.insert(actionIndexPair.second);
this->indexToActionMap.emplace(actionIndexPair.second, actionIndexPair.first);
}
// Build the mapping from action names to module indices so that the lookup can later be performed quickly.

20
src/storage/prism/Program.h
View File

@ -72,6 +72,15 @@ namespace storm {
*/
bool hasUndefinedConstants() const;
/*!
* Retrieves whether there are undefined constants appearing in any place other than the update probabilities
* of the commands and the reward expressions. This is to be used for parametric model checking where the
* parameters are only allowed to govern the probabilities, not the underlying graph of the model.
*
* @return True iff all undefined constants of the model only appear in update probabilities.
*/
bool hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards() const;
/*!
* Retrieves the undefined constants in the program.
*
@ -225,6 +234,14 @@ namespace storm {
*/
std::set<uint_fast64_t> const& getActionIndices() const;
/*!
* Retrieves the action name of the given action index.
*
* @param actionIndex The index of the action whose name to retrieve.
* @return The name of the action.
*/
std::string const& getActionName(uint_fast64_t actionIndex) const;
/*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the
* given action.
@ -442,6 +459,9 @@ namespace storm {
// A mapping from action names to their indices.
std::map<std::string, uint_fast64_t> actionToIndexMap;
// A mapping from action indices to their names.
std::map<uint_fast64_t, std::string> indexToActionMap;
// The set of actions present in this program.
std::set<std::string> actions;

14
src/storage/prism/RewardModel.cpp
View File

@ -45,6 +45,20 @@ namespace storm {
return RewardModel(this->getName(), newStateRewards, newTransitionRewards, this->getFilename(), this->getLineNumber());
}
bool RewardModel::containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
for (auto const& stateReward : this->getStateRewards()) {
if (stateReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
for (auto const& transitionReward : this->getTransitionRewards()) {
if (transitionReward.getStatePredicateExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
return true;
}
std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) {
stream << "rewards";
if (rewardModel.getName() != "") {

9
src/storage/prism/RewardModel.h
View File

@ -83,6 +83,15 @@ namespace storm {
*/
RewardModel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
/*!
* Checks whether any of the given variables only appear in the expressions defining the reward value.
*
* @param undefinedConstantVariables A set of variables that may only appear in the expressions defining the
* reward values.
* @return True iff the given variables only appear in the expressions defining the reward value.
*/
bool containsVariablesOnlyInRewardValueExpressions(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const;
friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);
private:

3
src/utility/cli.h
View File

@ -53,6 +53,9 @@ log4cplus::Logger printer;
#include "src/builder/ExplicitPrismModelBuilder.h"
#include "src/builder/DdPrismModelBuilder.h"
// Headers for DD-related classes.
#include "src/storage/dd/CuddDd.h"
// Headers for model processing.
#include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h"
#include "src/storage/DeterministicModelBisimulationDecomposition.h"

27
test/functional/builder/DdPrismModelBuilderTest.cpp
View File

@ -34,3 +34,30 @@ TEST(DdPrismModelBuilderTest, Dtmc) {
EXPECT_EQ(1728, model.first.getNonZeroCount());
EXPECT_EQ(2505, model.second.getNonZeroCount());
}
TEST(DdPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
std::pair<storm::dd::Dd<storm::dd::DdType::CUDD>, storm::dd::Dd<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(169, model.first.getNonZeroCount());
EXPECT_EQ(436, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(364, model.first.getNonZeroCount());
EXPECT_EQ(654, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(272, model.first.getNonZeroCount());
EXPECT_EQ(492, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(1038, model.first.getNonZeroCount());
EXPECT_EQ(1282, model.second.getNonZeroCount());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(4093, model.first.getNonZeroCount());
EXPECT_EQ(5585, model.second.getNonZeroCount());
}

28
test/functional/builder/ExplicitPrismModelBuilderTest.cpp
View File

@ -31,3 +31,31 @@ TEST(ExplicitPrismModelBuilderTest, Dtmc) {
EXPECT_EQ(1728, model->getNumberOfStates());
EXPECT_EQ(2505, model->getNumberOfTransitions());
}
TEST(ExplicitPrismModelBuilderTest, Mdp) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
std::unique_ptr<storm::models::AbstractModel<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(169, model->getNumberOfStates());
EXPECT_EQ(436, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(364, model->getNumberOfStates());
EXPECT_EQ(654, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(272, model->getNumberOfStates());
EXPECT_EQ(492, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(1038, model->getNumberOfStates());
EXPECT_EQ(1282, model->getNumberOfTransitions());
program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
EXPECT_EQ(4093, model->getNumberOfStates());
EXPECT_EQ(5585, model->getNumberOfTransitions());
}

60
test/functional/builder/coin2-2.nm
View File

@ -0,0 +1,60 @@
// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90]
// gxn/dxp 20/11/00
mdp
// constants
const int N=2;
const int K=2;
const int range = 2*(K+1)*N;
const int counter_init = (K+1)*N;
const int left = N;
const int right = 2*(K+1)*N - N;
// shared coin
global counter : [0..range] init counter_init;
module process1
// program counter
pc1 : [0..3];
// 0 - flip
// 1 - write
// 2 - check
// 3 - finished
// local coin
coin1 : [0..1];
// flip coin
[] (pc1=0) -> 0.5 : (coin1'=0) & (pc1'=1) + 0.5 : (coin1'=1) & (pc1'=1);
// write tails -1 (reset coin to add regularity)
[] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0);
// write heads +1 (reset coin to add regularity)
[] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0);
// check
// decide tails
[] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0);
// decide heads
[] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1);
// flip again
[] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0);
// loop (all loop together when done)
[done] (pc1=3) -> 1 : (pc1'=3);
endmodule
// construct remaining processes through renaming
module process2 = process1[pc1=pc2,coin1=coin2] endmodule
// labels
label "finished" = pc1=3 & pc2=3 ;
label "all_coins_equal_0" = coin1=0 & coin2=0 ;
label "all_coins_equal_1" = coin1=1 & coin2=1 ;
label "agree" = coin1=coin2 ;
// rewards
rewards "steps"
true : 1;
endrewards

130
test/functional/builder/csma2-2.nm
View File

@ -0,0 +1,130 @@
// CSMA/CD protocol - probabilistic version of kronos model (3 stations)
// gxn/dxp 04/12/01
mdp
// note made changes since cannot have strict inequalities
// in digital clocks approach and suppose a station only sends one message
// simplified parameters scaled
const int sigma=1; // time for messages to propagate along the bus
const int lambda=30; // time to send a message
// actual parameters
const int N = 2; // number of processes
const int K = 2; // exponential backoff limit
const int slot = 2*sigma; // length of slot
// const int M = floor(pow(2, K))-1 ; // max number of slots to wait
const int M = 3 ; // max number of slots to wait
//const int lambda=782;
//const int sigma=26;
// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1);
// formula min_collisions = min(cd1,cd2);
// formula max_collisions = max(cd1,cd2);
//----------------------------------------------------------------------------------------------------------------------------
// the bus
module bus
b : [0..2];
// b=0 - idle
// b=1 - active
// b=2 - collision
// clocks of bus
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy)
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected)
// a sender sends (ok - no other message being sent)
[send1] (b=0) -> (b'=1);
[send2] (b=0) -> (b'=1);
// a sender sends (bus busy - collision)
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2);
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2);
// finish sending
[end1] (b=1) -> (b'=0) & (y1'=0);
[end2] (b=1) -> (b'=0) & (y1'=0);
// bus busy
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b);
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b);
// collision detected
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0);
// time passage
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected)
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// model of first sender
module station1
// LOCAL STATE
s1 : [0..5];
// s1=0 - initial state
// s1=1 - transmit
// s1=2 - collision (set backoff)
// s1=3 - wait (bus busy)
// s1=4 - successfully sent
// LOCAL CLOCK
x1 : [0..max(lambda,slot)];
// BACKOFF COUNTER (number of slots to wait)
bc1 : [0..M];
// COLLISION COUNTER
cd1 : [0..K];
// start sending
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
// transmitting
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter)
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important
// set backoff (no time can pass in this state)
// probability depends on which transmission this is (cd1)
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ;
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ;
// wait until backoff counter reaches 0 then send again
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot)
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots)
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free)
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy)
// once finished nothing matters
[time] (s1>=4) -> (x1'=0);
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// construct further stations through renaming
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
//----------------------------------------------------------------------------------------------------------------------------
// reward structure for expected time
rewards "time"
[time] true : 1;
endrewards
//----------------------------------------------------------------------------------------------------------------------------
// labels/formulae
label "all_delivered" = s1=4&s2=4;
label "one_delivered" = s1=4|s2=4;
label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2);

170
test/functional/builder/firewire3-0.5.nm
View File

@ -0,0 +1,170 @@
// firewire protocol with integer semantics
// dxp/gxn 14/06/01
// CLOCKS
// x1 (x2) clock for node1 (node2)
// y1 and y2 (z1 and z2) clocks for wire12 (wire21)
mdp
// maximum and minimum delays
// fast
const int rc_fast_max = 85;
const int rc_fast_min = 76;
// slow
const int rc_slow_max = 167;
const int rc_slow_min = 159;
// delay caused by the wire length
const int delay = 3;
// probability of choosing fast
const double fast = 0.5;
const double slow=1-fast;
module wire12
// local state
w12 : [0..9];
// 0 - empty
// 1 - rec_req
// 2 - rec_req_ack
// 3 - rec_ack
// 4 - rec_ack_idle
// 5 - rec_idle
// 6 - rec_idle_req
// 7 - rec_ack_req
// 8 - rec_req_idle
// 9 - rec_idle_ack
// clock for wire12
y1 : [0..delay+1];
y2 : [0..delay+1];
// empty
// do not need y1 and y2 to increase as always reset when this state is left
// similarly can reset y1 and y2 when we re-enter this state
[snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0);
[snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0);
[snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0);
[time] w12=0 -> (w12'=w12);
// rec_req
[snd_req12] w12=1 -> (w12'=1);
[rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0);
[snd_ack12] w12=1 -> (w12'=2) & (y2'=0);
[snd_idle12] w12=1 -> (w12'=8) & (y2'=0);
[time] w12=1 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_req_ack
[snd_ack12] w12=2 -> (w12'=2);
[rec_req12] w12=2 -> (w12'=3);
[time] w12=2 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_ack
[snd_ack12] w12=3 -> (w12'=3);
[rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0);
[snd_idle12] w12=3 -> (w12'=4) & (y2'=0);
[snd_req12] w12=3 -> (w12'=7) & (y2'=0);
[time] w12=3 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_ack_idle
[snd_idle12] w12=4 -> (w12'=4);
[rec_ack12] w12=4 -> (w12'=5);
[time] w12=4 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_idle
[snd_idle12] w12=5 -> (w12'=5);
[rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0);
[snd_req12] w12=5 -> (w12'=6) & (y2'=0);
[snd_ack12] w12=5 -> (w12'=9) & (y2'=0);
[time] w12=5 & y2<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_idle_req
[snd_req12] w12=6 -> (w12'=6);
[rec_idle12] w12=6 -> (w12'=1);
[time] w12=6 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_ack_req
[snd_req12] w12=7 -> (w12'=7);
[rec_ack12] w12=7 -> (w12'=1);
[time] w12=7 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_req_idle
[snd_idle12] w12=8 -> (w12'=8);
[rec_req12] w12=8 -> (w12'=5);
[time] w12=8 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
// rec_idle_ack
[snd_ack12] w12=9 -> (w12'=9);
[rec_idle12] w12=9 -> (w12'=3);
[time] w12=9 & y1<delay -> (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1));
endmodule
module node1
// clock for node1
x1 : [0..168];
// local state
s1 : [0..8];
// 0 - root contention
// 1 - rec_idle
// 2 - rec_req_fast
// 3 - rec_req_slow
// 4 - rec_idle_fast
// 5 - rec_idle_slow
// 6 - snd_req
// 7- almost_root
// 8 - almost_child
// added resets to x1 when not considered again until after rest
// removed root and child (using almost root and almost child)
// root contention immediate state)
[snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0);
[rec_idle21] s1=0 -> (s1'=1);
// rec_idle immediate state)
[snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (s1'=5) & (x1'=0);
[rec_req21] s1=1 -> (s1'=0);
// rec_req_fast
[rec_idle21] s1=2 -> (s1'=4);
[snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0);
[time] s1=2 & x1<rc_fast_max -> (x1'=min(x1+1,168));
// rec_req_slow
[rec_idle21] s1=3 -> (s1'=5);
[snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0);
[time] s1=3 & x1<rc_slow_max -> (x1'=min(x1+1,168));
// rec_idle_fast
[rec_req21] s1=4 -> (s1'=2);
[snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0);
[time] s1=4 & x1<rc_fast_max -> (x1'=min(x1+1,168));
// rec_idle_slow
[rec_req21] s1=5 -> (s1'=3);
[snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0);
[time] s1=5 & x1<rc_slow_max -> (x1'=min(x1+1,168));
// snd_req
// do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1
// also can set x1 to 0 upon entering this state
[rec_req21] s1=6 -> (s1'=0);
[rec_ack21] s1=6 -> (s1'=8);
[time] s1=6 -> (s1'=s1);
// almost root (immediate)
// loop in final states to remove deadlock
[] s1=7 & s2=8 -> (s1'=s1);
[] s1=8 & s2=7 -> (s1'=s1);
[time] s1=7 -> (s1'=s1);
[time] s1=8 -> (s1'=s1);
endmodule
// construct remaining automata through renaming
module wire21=wire12[w12=w21, y1=z1, y2=z2,
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21,
rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21]
endmodule
module node2=node1[s1=s2, s2=s1, x1=x2,
rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12,
snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21]
endmodule
// reward structures
// time
rewards "time"
[time] true : 1;
endrewards
// time nodes sending
rewards "time_sending"
[time] (w12>0 | w21>0) : 1;
endrewards
label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8));

91
test/functional/builder/leader3.nm
View File

@ -0,0 +1,91 @@
// asynchronous leader election
// 4 processes
// gxn/dxp 29/01/01
mdp
const int N = 3; // number of processes
//----------------------------------------------------------------------------------------------------------------------------
module process1
// COUNTER
c1 : [0..3-1];
// STATES
s1 : [0..4];
// 0 make choice
// 1 have not received neighbours choice
// 2 active
// 3 inactive
// 4 leader
// PREFERENCE
p1 : [0..1];
// VARIABLES FOR SENDING AND RECEIVING
receive1 : [0..2];
// not received anything
// received choice
// received counter
sent1 : [0..2];
// not send anything
// sent choice
// sent counter
// pick value
[] (s1=0) -> 0.5 : (s1'=1) & (p1'=0) + 0.5 : (s1'=1) & (p1'=1);
// send preference
[p12] (s1=1) & (sent1=0) -> (sent1'=1);
// receive preference
// stay active
[p31] (s1=1) & (receive1=0) & !( (p1=0) & (p3=1) ) -> (s1'=2) & (receive1'=1);
// become inactive
[p31] (s1=1) & (receive1=0) & (p1=0) & (p3=1) -> (s1'=3) & (receive1'=1);
// send preference (can now reset preference)
[p12] (s1=2) & (sent1=0) -> (sent1'=1) & (p1'=0);
// send counter (already sent preference)
// not received counter yet
[c12] (s1=2) & (sent1=1) & (receive1=1) -> (sent1'=2);
// received counter (pick again)
[c12] (s1=2) & (sent1=1) & (receive1=2) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
// receive counter and not sent yet (note in this case do not pass it on as will send own counter)
[c31] (s1=2) & (receive1=1) & (sent1<2) -> (receive1'=2);
// receive counter and sent counter
// only active process (decide)
[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3=N-1) -> (s1'=4) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
// other active process (pick again)
[c31] (s1=2) & (receive1=1) & (sent1=2) & (c3<N-1) -> (s1'=0) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
// send preference (must have received preference) and can now reset
[p12] (s1=3) & (receive1>0) & (sent1=0) -> (sent1'=1) & (p1'=0);
// send counter (must have received counter first) and can now reset
[c12] (s1=3) & (receive1=2) & (sent1=1) -> (s1'=3) & (p1'=0) & (c1'=0) & (sent1'=0) & (receive1'=0);
// receive preference
[p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1);
// receive counter
[c31] (s1=3) & (receive1=1) & (c3<N-1) -> (c1'=c3+1) & (receive1'=2);
// done
[done] (s1=4) -> (s1'=s1);
// add loop for processes who are inactive
[done] (s1=3) -> (s1'=s1);
endmodule
//----------------------------------------------------------------------------------------------------------------------------
// construct further stations through renaming
module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule
module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule
//----------------------------------------------------------------------------------------------------------------------------
//----------------------------------------------------------------------------------------------------------------------------
formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0);
label "elected" = s1=4|s2=4|s3=4;

40
test/functional/builder/two_dice.nm
View File

@ -0,0 +1,40 @@
// sum of two dice as the asynchronous parallel composition of
// two copies of Knuth's model of a fair die using only fair coins
mdp
module die1
// local state
s1 : [0..7] init 0;
// value of the dice
d1 : [0..6] init 0;
[] s1=0 -> 0.5 : (s1'=1) + 0.5 : (s1'=2);
[] s1=1 -> 0.5 : (s1'=3) + 0.5 : (s1'=4);
[] s1=2 -> 0.5 : (s1'=5) + 0.5 : (s1'=6);
[] s1=3 -> 0.5 : (s1'=1) + 0.5 : (s1'=7) & (d1'=1);
[] s1=4 -> 0.5 : (s1'=7) & (d1'=2) + 0.5 : (s1'=7) & (d1'=3);
[] s1=5 -> 0.5 : (s1'=7) & (d1'=4) + 0.5 : (s1'=7) & (d1'=5);
[] s1=6 -> 0.5 : (s1'=2) + 0.5 : (s1'=7) & (d1'=6);
[] s1=7 & s2=7 -> 1: (s1'=7);
endmodule
module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule
rewards "coinflips"
[] s1<7 | s2<7 : 1;
endrewards
label "done" = s1=7 & s2=7;
label "two" = s1=7 & s2=7 & d1+d2=2;
label "three" = s1=7 & s2=7 & d1+d2=3;
label "four" = s1=7 & s2=7 & d1+d2=4;
label "five" = s1=7 & s2=7 & d1+d2=5;
label "six" = s1=7 & s2=7 & d1+d2=6;
label "seven" = s1=7 & s2=7 & d1+d2=7;
label "eight" = s1=7 & s2=7 & d1+d2=8;
label "nine" = s1=7 & s2=7 & d1+d2=9;
label "ten" = s1=7 & s2=7 & d1+d2=10;
label "eleven" = s1=7 & s2=7 & d1+d2=11;
label "twelve" = s1=7 & s2=7 & d1+d2=12;

13
wlan0_collide.nm
View File

@ -0,0 +1,13 @@
mdp
module station1
s1 : [0..12] init 0;
// [] s1=0 -> (s1'=8) ;
[] s1=1 -> (s1'=1);
[] s1=1 -> (s1'=1);
//[] s1=8 -> (s1'=8);
endmodule
Write Preview
|||||||
100:0
Loading…
Cancel
Save