1228 std::set<storm::expressions::Variable> all;
1229 std::set<storm::expressions::Variable> allGlobals;
1230 std::set<storm::expressions::Variable> globalVariables;
1231 std::set<storm::expressions::Variable> constants;
1232 for (
auto const& constant : this->getConstants()) {
1234 if (constant.isDefined()) {
1235 std::set<storm::expressions::Variable> containedVariables = constant.getExpression().getVariables();
1236 std::set<storm::expressions::Variable> illegalVariables;
1237 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1238 std::inserter(illegalVariables, illegalVariables.begin()));
1239 bool isValid = illegalVariables.empty();
1242 std::vector<std::string> illegalVariableNames;
1243 for (
auto const& var : illegalVariables) {
1244 illegalVariableNames.push_back(var.getName());
1247 "Error in " << constant.getFilename() <<
", line " << constant.getLineNumber()
1248 <<
": defining expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",")
1254 constants.insert(constant.getExpressionVariable());
1255 all.insert(constant.getExpressionVariable());
1256 allGlobals.insert(constant.getExpressionVariable());
1260 std::set<storm::expressions::Variable> variables;
1261 for (
auto const& variable : this->getGlobalBooleanVariables()) {
1262 if (variable.hasInitialValue()) {
1263 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1264 "Error for " << variable.getName() <<
" (" << variable.getFilename() <<
", line " << variable.getLineNumber()
1265 <<
"): illegal to specify initial value if an initial construct is present.");
1268 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1269 std::set<storm::expressions::Variable> illegalVariables;
1270 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1271 std::inserter(illegalVariables, illegalVariables.begin()));
1272 bool isValid = illegalVariables.empty();
1275 std::vector<std::string> illegalVariableNames;
1276 for (
auto const& var : illegalVariables) {
1277 illegalVariableNames.push_back(var.getName());
1280 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1281 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1287 variables.insert(variable.getExpressionVariable());
1288 all.insert(variable.getExpressionVariable());
1289 allGlobals.insert(variable.getExpressionVariable());
1290 globalVariables.insert(variable.getExpressionVariable());
1292 for (
auto const& variable : this->getGlobalIntegerVariables()) {
1294 if (variable.hasLowerBoundExpression()) {
1295 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1296 std::set<storm::expressions::Variable> illegalVariables;
1297 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1298 std::inserter(illegalVariables, illegalVariables.begin()));
1299 bool isValid = illegalVariables.empty();
1302 std::vector<std::string> illegalVariableNames;
1303 for (
auto const& var : illegalVariables) {
1304 illegalVariableNames.push_back(var.getName());
1307 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1308 <<
": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1313 if (variable.hasUpperBoundExpression()) {
1314 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1315 std::set<storm::expressions::Variable> illegalVariables;
1316 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1317 std::inserter(illegalVariables, illegalVariables.begin()));
1318 bool isValid = illegalVariables.empty();
1320 std::vector<std::string> illegalVariableNames;
1321 for (
auto const& var : illegalVariables) {
1322 illegalVariableNames.push_back(var.getName());
1325 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1326 <<
": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1331 if (variable.hasInitialValue()) {
1332 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1333 "Error for " << variable.getName() <<
" (" << variable.getFilename() <<
", line " << variable.getLineNumber()
1334 <<
"): illegal to specify initial value if an initial construct is present.");
1337 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1338 std::set<storm::expressions::Variable> illegalVariables;
1339 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1340 std::inserter(illegalVariables, illegalVariables.begin()));
1341 bool isValid = illegalVariables.empty();
1343 std::vector<std::string> illegalVariableNames;
1344 for (
auto const& var : illegalVariables) {
1345 illegalVariableNames.push_back(var.getName());
1348 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1349 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1355 variables.insert(variable.getExpressionVariable());
1356 all.insert(variable.getExpressionVariable());
1357 allGlobals.insert(variable.getExpressionVariable());
1358 globalVariables.insert(variable.getExpressionVariable());
1362 for (
auto const& module : this->getModules()) {
1363 for (
auto const& variable :
module.getBooleanVariables()) {
1364 if (variable.hasInitialValue()) {
1365 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1366 "Error for " << module.getName() << "." << variable.getName() << " (" << variable.getFilename() << ", line "
1367 << variable.getLineNumber() << "): illegal to specify initial value if an initial construct is present.");
1370 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1371 std::set<storm::expressions::Variable> illegalVariables;
1372 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1373 std::inserter(illegalVariables, illegalVariables.begin()));
1374 bool isValid = illegalVariables.empty();
1376 std::vector<std::string> illegalVariableNames;
1377 for (
auto const& var : illegalVariables) {
1378 illegalVariableNames.push_back(var.getName());
1381 isValid, storm::exceptions::WrongFormatException,
1382 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1383 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1388 variables.insert(variable.getExpressionVariable());
1389 all.insert(variable.getExpressionVariable());
1391 for (
auto const& variable : module.getIntegerVariables()) {
1393 if (variable.hasLowerBoundExpression()) {
1394 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1395 std::set<storm::expressions::Variable> illegalVariables;
1396 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1397 std::inserter(illegalVariables, illegalVariables.begin()));
1398 bool isValid = illegalVariables.empty();
1400 std::vector<std::string> illegalVariableNames;
1401 for (
auto const& var : illegalVariables) {
1402 illegalVariableNames.push_back(var.getName());
1405 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1406 <<
": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1411 if (variable.hasUpperBoundExpression()) {
1412 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1413 std::set<storm::expressions::Variable> illegalVariables;
1415 illegalVariables.clear();
1416 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1417 std::inserter(illegalVariables, illegalVariables.begin()));
1418 bool isValid = illegalVariables.empty();
1420 std::vector<std::string> illegalVariableNames;
1421 for (
auto const& var : illegalVariables) {
1422 illegalVariableNames.push_back(var.getName());
1425 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1426 <<
": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1431 if (variable.hasInitialValue()) {
1432 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1433 "Error for " << module.getName() <<
"." << variable.getName() <<
" (" << variable.getFilename() <<
", line "
1434 << variable.getLineNumber() <<
"): illegal to specify initial value if an initial construct is present.");
1437 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1438 std::set<storm::expressions::Variable> illegalVariables;
1439 illegalVariables.clear();
1440 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1441 std::inserter(illegalVariables, illegalVariables.begin()));
1442 bool isValid = illegalVariables.empty();
1444 std::vector<std::string> illegalVariableNames;
1445 for (
auto const& var : illegalVariables) {
1446 illegalVariableNames.push_back(var.getName());
1449 isValid, storm::exceptions::WrongFormatException,
1450 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1451 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1456 variables.insert(variable.getExpressionVariable());
1457 all.insert(variable.getExpressionVariable());
1460 for (
auto const& variable : module.getClockVariables()) {
1462 variables.insert(variable.getExpressionVariable());
1463 all.insert(variable.getExpressionVariable());
1468 std::set<storm::expressions::Variable> variablesAndConstants;
1469 std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
1472 for (
auto const& formula : this->getFormulas()) {
1473 std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
1474 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1476 "Error in " << formula.getFilename() <<
", line " << formula.getLineNumber() <<
": expression '" << formula.getExpression()
1477 <<
"'of formula '" << formula.getName() <<
"' refers to unknown identifiers.");
1478 if (formula.hasExpressionVariable()) {
1479 all.insert(formula.getExpressionVariable());
1480 variablesAndConstants.insert(formula.getExpressionVariable());
1485 bool hasProbabilisticCommand =
false;
1486 bool hasMarkovianCommand =
false;
1487 bool hasLabeledMarkovianCommand =
false;
1488 std::map<std::pair<storm::expressions::Variable, uint64_t>, std::pair<uint64_t, std::string>> writtenGlobalVariables;
1489 for (
auto const& module : this->getModules()) {
1490 std::set<storm::expressions::Variable> legalVariables = globalVariables;
1491 for (
auto const& variable : module.getBooleanVariables()) {
1492 legalVariables.insert(variable.getExpressionVariable());
1494 for (
auto const& variable : module.getIntegerVariables()) {
1495 legalVariables.insert(variable.getExpressionVariable());
1497 for (
auto const& variable : module.getClockVariables()) {
1498 legalVariables.insert(variable.getExpressionVariable());
1501 if (module.hasInvariant()) {
1502 std::set<storm::expressions::Variable> containedVariables =
module.getInvariant().getVariables();
1503 std::set<storm::expressions::Variable> illegalVariables;
1504 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1505 std::inserter(illegalVariables, illegalVariables.begin()));
1506 bool isValid = illegalVariables.empty();
1508 std::vector<std::string> illegalVariableNames;
1509 for (
auto const& var : illegalVariables) {
1510 illegalVariableNames.push_back(var.getName());
1513 "Error in " << module.getFilename() <<
", line " << module.getLineNumber() <<
": invariant " << module.getInvariant()
1514 <<
" refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1516 STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException,
1517 "Error in " << module.getFilename() <<
", line " << module.getLineNumber() <<
": invariant " << module.getInvariant()
1518 <<
" must evaluate to type 'bool'.");
1521 for (
auto& command : module.getCommands()) {
1523 std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
1524 std::set<storm::expressions::Variable> illegalVariables;
1525 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1526 std::inserter(illegalVariables, illegalVariables.begin()));
1527 bool isValid = illegalVariables.empty();
1529 std::vector<std::string> illegalVariableNames;
1530 for (
auto const& var : illegalVariables) {
1531 illegalVariableNames.push_back(var.getName());
1534 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": guard " << command.getGuardExpression()
1535 <<
" refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1538 command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1539 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": expression for guard must evaluate to type 'bool'.");
1542 if (command.isMarkovian()) {
1543 hasMarkovianCommand =
true;
1545 hasProbabilisticCommand =
true;
1550 if (command.isMarkovian() && command.isLabeled()) {
1551 hasLabeledMarkovianCommand =
true;
1555 for (
auto const& update : command.getUpdates()) {
1556 containedVariables = update.getLikelihoodExpression().getVariables();
1557 illegalVariables.clear();
1558 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1559 std::inserter(illegalVariables, illegalVariables.begin()));
1560 isValid = illegalVariables.empty();
1562 std::vector<std::string> illegalVariableNames;
1563 for (
auto const& var : illegalVariables) {
1564 illegalVariableNames.push_back(var.getName());
1567 isValid, storm::exceptions::WrongFormatException,
1568 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1569 <<
": likelihood expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1573 std::set<storm::expressions::Variable> alreadyAssignedVariables;
1574 for (
auto const& assignment : update.getAssignments()) {
1577 if (legalVariables.find(assignedVariable) == legalVariables.end()) {
1578 if (all.find(assignedVariable) != all.end()) {
1580 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1581 <<
": assignment illegally refers to variable '" << assignment.getVariableName() <<
"'.");
1584 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1585 <<
": assignment refers to unknown variable '" << assignment.getVariableName() <<
"'.");
1588 STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException,
1589 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": duplicate assignment to variable '"
1590 << assignment.getVariableName() <<
"'.");
1592 (assignedVariable.
getType().
isRationalType() && assignment.getExpression().getType().isNumericalType()),
1593 storm::exceptions::WrongFormatException,
1594 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": illegally assigning a value of type '"
1595 << assignment.getExpression().getType() <<
"' to variable '" << assignment.getVariableName() <<
"' of type '"
1596 << assignedVariable.
getType() <<
"'.");
1598 if (command.isLabeled() && globalVariables.find(assignedVariable) != globalVariables.end()) {
1599 std::pair<storm::expressions::Variable, uint64_t> variableActionIndexPair(assignedVariable, command.getActionIndex());
1600 std::pair<uint64_t, std::string> lineModuleNamePair(command.getLineNumber(), module.getName());
1601 auto insertionResult = writtenGlobalVariables.emplace(variableActionIndexPair, lineModuleNamePair);
1603 insertionResult.second || insertionResult.first->second.second == module.getName(), storm::exceptions::WrongFormatException,
1604 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": Syncronizing command with action label '"
1605 << command.getActionName() <<
"' illegally assigns a value to global variable '" << assignedVariable.
getName()
1606 <<
"'. Previous assignment to the variable at line " << insertionResult.first->second.first <<
" in module '"
1607 << insertionResult.first->second.second <<
"'.");
1610 containedVariables = assignment.getExpression().getVariables();
1611 illegalVariables.clear();
1612 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1613 std::inserter(illegalVariables, illegalVariables.begin()));
1614 isValid = illegalVariables.empty();
1616 std::vector<std::string> illegalVariableNames;
1617 for (
auto const& var : illegalVariables) {
1618 illegalVariableNames.push_back(var.getName());
1621 isValid, storm::exceptions::WrongFormatException,
1622 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1623 <<
": assigned expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1627 alreadyAssignedVariables.insert(assignedVariable);
1633 if (hasLabeledMarkovianCommand) {
1634 if (prismCompatibility) {
1636 false,
"The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1639 "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1644 STORM_LOG_THROW(!hasMarkovianCommand, storm::exceptions::WrongFormatException,
"Discrete-time model must not have Markovian commands.");
1645 }
else if (this->
getModelType() == Program::ModelType::CTMC) {
1646 STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException,
1647 "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn "
1648 "on the PRISM compatibility mode using the flag '-pc'.");
1652 for (
auto const& rewardModel : this->getRewardModels()) {
1653 for (
auto const& stateReward : rewardModel.getStateRewards()) {
1654 std::set<storm::expressions::Variable> containedVariables = stateReward.getStatePredicateExpression().getVariables();
1655 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1657 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber()
1658 <<
": state reward expression refers to unknown identifiers.");
1660 stateReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1661 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber() <<
": state predicate must evaluate to type 'bool'.");
1663 containedVariables = stateReward.getRewardValueExpression().getVariables();
1664 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1666 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber()
1667 <<
": state reward value expression refers to unknown identifiers.");
1668 STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1669 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber()
1670 <<
": reward value expression must evaluate to numerical type.");
1673 for (
auto const& stateActionReward : rewardModel.getStateActionRewards()) {
1674 std::set<storm::expressions::Variable> containedVariables = stateActionReward.getStatePredicateExpression().getVariables();
1675 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1677 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1678 <<
": state reward expression refers to unknown identifiers.");
1679 STORM_LOG_THROW(stateActionReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1680 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1681 <<
": state predicate must evaluate to type 'bool'.");
1683 containedVariables = stateActionReward.getRewardValueExpression().getVariables();
1684 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1686 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1687 <<
": state reward value expression refers to unknown identifiers.");
1688 STORM_LOG_THROW(stateActionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1689 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1690 <<
": reward value expression must evaluate to numerical type.");
1693 for (
auto const& transitionReward : rewardModel.getTransitionRewards()) {
1694 std::set<storm::expressions::Variable> containedVariables = transitionReward.getSourceStatePredicateExpression().getVariables();
1695 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1697 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1698 <<
": state reward expression refers to unknown identifiers.");
1699 STORM_LOG_THROW(transitionReward.getSourceStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1700 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1701 <<
": state predicate must evaluate to type 'bool'.");
1703 containedVariables = transitionReward.getTargetStatePredicateExpression().getVariables();
1704 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1706 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1707 <<
": state reward expression refers to unknown identifiers.");
1708 STORM_LOG_THROW(transitionReward.getTargetStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1709 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1710 <<
": state predicate must evaluate to type 'bool'.");
1712 containedVariables = transitionReward.getRewardValueExpression().getVariables();
1713 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1715 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1716 <<
": state reward value expression refers to unknown identifiers.");
1717 STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1718 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1719 <<
": reward value expression must evaluate to numerical type.");
1724 if (this->hasInitialConstruct()) {
1725 std::set<storm::expressions::Variable> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
1726 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
1728 "Error in " << this->getInitialConstruct().getFilename() <<
", line " << this->getInitialConstruct().getLineNumber()
1729 <<
": initial construct refers to unknown identifiers.");
1733 if (systemCompositionConstruct) {
1734 CompositionValidityChecker checker(*
this);
1735 checker.check(systemCompositionConstruct.get().getSystemComposition());
1739 for (
auto const& label : this->getLabels()) {
1740 std::set<storm::expressions::Variable> containedVariables = label.getStatePredicateExpression().getVariables();
1741 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1743 "Error in " << label.getFilename() <<
", line " << label.getLineNumber() <<
": label expression refers to unknown identifiers.");
1744 STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1745 "Error in " << label.getFilename() <<
", line " << label.getLineNumber() <<
": label predicate must evaluate to type 'bool'.");
1749 for (
auto const& player : this->getPlayers()) {
1751 for (
auto const& controlledAction : player.getActions()) {
1752 STORM_LOG_THROW(this->hasAction(controlledAction), storm::exceptions::InternalException,
1753 "Error in " << player.getFilename() <<
", line " << player.getLineNumber() <<
": The player controlled action " << controlledAction
1754 <<
" is not available.");
1756 for (
auto const& controlledModule : player.getModules()) {
1758 "Error in " << player.getFilename() <<
", line " << player.getLineNumber() <<
": The player controlled module " << controlledModule
1759 <<
" is not available.");
1763 if (lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
1765 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
1766 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
1767 for (
auto const& module : this->getModules()) {
1768 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
1769 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
1770 for (
auto const& command : module.getCommands()) {
1771 if (!command.isLabeled())
1773 for (
auto const& update : command.getUpdates()) {
1774 for (
auto const& assignment : update.getAssignments()) {
1775 if (this->globalBooleanVariableExists(assignment.getVariable().getName())) {
1776 globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1777 }
else if (this->globalIntegerVariableExists(assignment.getVariable().getName())) {
1778 globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1783 for (
auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
1784 if (globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
1786 "Error in " << module.getFilename() <<
", line " << module.getLineNumber()
1787 <<
": assignment of (possibly) synchronizing command with label '" << entry.second
1788 <<
"' writes to global variable '" << entry.first <<
"'.");
1791 for (
auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
1792 if (globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
1794 "Error in " << module.getFilename() <<
", line " << module.getLineNumber()
1795 <<
": assignment of (possibly) synchronizing command with label '" << entry.second
1796 <<
"' writes to global variable '" << entry.first <<
"'.");
1951Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory>
const& smtSolverFactory)
const {
1953 if (this->getNumberOfModules() == 1) {
1957 STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException,
1958 "Unable to flatten modules for model of type '" << this->getModelType() <<
"'.");
1963 std::unique_ptr<storm::solver::SmtSolver> solver = smtSolverFactory->create(*manager);
1966 std::stringstream newModuleName;
1967 std::vector<storm::prism::BooleanVariable> allBooleanVariables;
1968 std::vector<storm::prism::IntegerVariable> allIntegerVariables;
1969 std::vector<storm::prism::ClockVariable> allClockVariables;
1970 std::vector<storm::prism::Command> newCommands;
1971 uint_fast64_t nextCommandIndex = 0;
1972 uint_fast64_t nextUpdateIndex = 0;
1975 for (
auto const& constant : this->getConstants()) {
1976 if (constant.isDefined()) {
1977 if (constant.getType().isBooleanType()) {
1980 solver->add(constant.getExpressionVariable() == constant.getExpression());
1986 for (
auto const& variable : this->getGlobalIntegerVariables()) {
1987 solver->add(variable.getRangeExpression());
1992 allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
1993 allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
1998 for (
auto const& module : this->getModules()) {
1999 newModuleName <<
module.getName() << "_";
2000 allBooleanVariables.insert(allBooleanVariables.end(),
module.getBooleanVariables().begin(), module.getBooleanVariables().end());
2001 allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
2002 allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
2004 for (
auto const& variable :
module.getIntegerVariables()) {
2005 solver->add(variable.getRangeExpression());
2008 if (module.hasInvariant()) {
2009 newInvariant = newInvariant.
isInitialized() ? (newInvariant &&
module.getInvariant()) : module.getInvariant();
2014 for (
auto const& command :
module.getCommands()) {
2015 if (!command.isLabeled()) {
2016 std::vector<storm::prism::Update> updates;
2017 updates.reserve(command.getUpdates().size());
2019 for (
auto const& update : command.getUpdates()) {
2021 storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0));
2025 newCommands.push_back(
storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find(
"")->second,
"",
2026 command.getGuardExpression(), updates, command.getFilename(), 0));
2038 for (
auto const& actionIndex : this->getSynchronizingActionIndices()) {
2039 bool noCombinationsForAction =
false;
2042 std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> possibleCommands;
2044 for (
auto const& module : this->getModules()) {
2046 if (!module.hasActionIndex(actionIndex)) {
2050 std::set<uint_fast64_t>
const& commandIndices =
module.getCommandIndicesByActionIndex(actionIndex);
2054 if (commandIndices.empty()) {
2055 noCombinationsForAction =
true;
2060 possibleCommands.push_back(std::vector<std::reference_wrapper<storm::prism::Command const>>());
2063 for (
auto const& commandIndex : commandIndices) {
2064 possibleCommands.back().push_back(module.getCommand(commandIndex));
2070 if (!noCombinationsForAction) {
2075 std::vector<std::vector<storm::expressions::Variable>> commandVariables(possibleCommands.size());
2076 std::vector<storm::expressions::Variable> allCommandVariables;
2077 for (uint_fast64_t outerIndex = 0; outerIndex < possibleCommands.size(); ++outerIndex) {
2079 for (uint_fast64_t innerIndex = 0; innerIndex < possibleCommands[outerIndex].size(); ++innerIndex) {
2080 commandVariables[outerIndex].push_back(
manager->declareFreshBooleanVariable());
2081 allCommandVariables.push_back(commandVariables[outerIndex].back());
2082 solver->add(
implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression()));
2086 for (
auto const& commandVariable : commandVariables[outerIndex]) {
2087 atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable;
2089 solver->add(atLeastOneCommandFromModule);
2098 std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
2100 for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
2101 for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
2102 if (modelReference.
getBooleanValue(commandVariables[outerIndex][innerIndex])) {
2103 chosenCommands[outerIndex].push_back(possibleCommands[outerIndex][innerIndex]);
2110 std::vector<std::vector<std::reference_wrapper<Command const>>::const_iterator> iterators;
2111 for (
auto const& element : chosenCommands) {
2112 iterators.push_back(element.begin());
2115 bool movedAtLeastOneIterator =
false;
2116 std::vector<std::reference_wrapper<Command const>> commandCombination(chosenCommands.size(), chosenCommands.front().front());
2117 std::vector<uint_fast64_t> commandCombinationIndices(iterators.size());
2119 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2120 commandCombination[index] = *iterators[index];
2121 commandCombinationIndices[index] = commandCombination[index].get().getGlobalIndex();
2125 auto seenIt = seenCommandCombinations.find(commandCombinationIndices);
2126 if (seenIt == seenCommandCombinations.end()) {
2127 newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second,
2128 commandCombination));
2129 seenCommandCombinations.insert(commandCombinationIndices);
2133 nextUpdateIndex += newCommands.back().getNumberOfUpdates();
2136 movedAtLeastOneIterator =
false;
2137 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2139 if (iterators[index] != chosenCommands[index].cend()) {
2140 movedAtLeastOneIterator =
true;
2143 iterators[index] = chosenCommands[index].cbegin();
2146 }
while (movedAtLeastOneIterator);
2156 storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands,
2157 this->getFilename(), 0);
2159 return Program(manager, this->
getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(),
2160 std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), this->getPlayers(), {singleModule}, actionToIndexMap,
2161 this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(),
2162 this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0,
true);