1241 std::set<storm::expressions::Variable> all;
1242 std::set<storm::expressions::Variable> allGlobals;
1243 std::set<storm::expressions::Variable> globalVariables;
1244 std::set<storm::expressions::Variable> constants;
1245 for (
auto const& constant : this->getConstants()) {
1247 if (constant.isDefined()) {
1248 std::set<storm::expressions::Variable> containedVariables = constant.getExpression().getVariables();
1249 std::set<storm::expressions::Variable> illegalVariables;
1250 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1251 std::inserter(illegalVariables, illegalVariables.begin()));
1252 bool isValid = illegalVariables.empty();
1255 std::vector<std::string> illegalVariableNames;
1256 for (
auto const& var : illegalVariables) {
1257 illegalVariableNames.push_back(var.getName());
1260 "Error in " << constant.getFilename() <<
", line " << constant.getLineNumber()
1261 <<
": defining expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",")
1267 constants.insert(constant.getExpressionVariable());
1268 all.insert(constant.getExpressionVariable());
1269 allGlobals.insert(constant.getExpressionVariable());
1273 std::set<storm::expressions::Variable> variables;
1274 for (
auto const& variable : this->getGlobalBooleanVariables()) {
1275 if (variable.hasInitialValue()) {
1276 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1277 "Error for " << variable.getName() <<
" (" << variable.getFilename() <<
", line " << variable.getLineNumber()
1278 <<
"): illegal to specify initial value if an initial construct is present.");
1281 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1282 std::set<storm::expressions::Variable> illegalVariables;
1283 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1284 std::inserter(illegalVariables, illegalVariables.begin()));
1285 bool isValid = illegalVariables.empty();
1288 std::vector<std::string> illegalVariableNames;
1289 for (
auto const& var : illegalVariables) {
1290 illegalVariableNames.push_back(var.getName());
1293 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1294 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1300 variables.insert(variable.getExpressionVariable());
1301 all.insert(variable.getExpressionVariable());
1302 allGlobals.insert(variable.getExpressionVariable());
1303 globalVariables.insert(variable.getExpressionVariable());
1305 for (
auto const& variable : this->getGlobalIntegerVariables()) {
1307 if (variable.hasLowerBoundExpression()) {
1308 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1309 std::set<storm::expressions::Variable> illegalVariables;
1310 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1311 std::inserter(illegalVariables, illegalVariables.begin()));
1312 bool isValid = illegalVariables.empty();
1315 std::vector<std::string> illegalVariableNames;
1316 for (
auto const& var : illegalVariables) {
1317 illegalVariableNames.push_back(var.getName());
1320 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1321 <<
": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1326 if (variable.hasUpperBoundExpression()) {
1327 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1328 std::set<storm::expressions::Variable> illegalVariables;
1329 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1330 std::inserter(illegalVariables, illegalVariables.begin()));
1331 bool isValid = illegalVariables.empty();
1333 std::vector<std::string> illegalVariableNames;
1334 for (
auto const& var : illegalVariables) {
1335 illegalVariableNames.push_back(var.getName());
1338 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1339 <<
": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1344 if (variable.hasInitialValue()) {
1345 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1346 "Error for " << variable.getName() <<
" (" << variable.getFilename() <<
", line " << variable.getLineNumber()
1347 <<
"): illegal to specify initial value if an initial construct is present.");
1350 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1351 std::set<storm::expressions::Variable> illegalVariables;
1352 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1353 std::inserter(illegalVariables, illegalVariables.begin()));
1354 bool isValid = illegalVariables.empty();
1356 std::vector<std::string> illegalVariableNames;
1357 for (
auto const& var : illegalVariables) {
1358 illegalVariableNames.push_back(var.getName());
1361 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1362 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1368 variables.insert(variable.getExpressionVariable());
1369 all.insert(variable.getExpressionVariable());
1370 allGlobals.insert(variable.getExpressionVariable());
1371 globalVariables.insert(variable.getExpressionVariable());
1375 for (
auto const& module : this->getModules()) {
1376 for (
auto const& variable :
module.getBooleanVariables()) {
1377 if (variable.hasInitialValue()) {
1378 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1379 "Error for " << module.getName() << "." << variable.getName() << " (" << variable.getFilename() << ", line "
1380 << variable.getLineNumber() << "): illegal to specify initial value if an initial construct is present.");
1383 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1384 std::set<storm::expressions::Variable> illegalVariables;
1385 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1386 std::inserter(illegalVariables, illegalVariables.begin()));
1387 bool isValid = illegalVariables.empty();
1389 std::vector<std::string> illegalVariableNames;
1390 for (
auto const& var : illegalVariables) {
1391 illegalVariableNames.push_back(var.getName());
1394 isValid, storm::exceptions::WrongFormatException,
1395 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1396 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1401 variables.insert(variable.getExpressionVariable());
1402 all.insert(variable.getExpressionVariable());
1404 for (
auto const& variable : module.getIntegerVariables()) {
1406 if (variable.hasLowerBoundExpression()) {
1407 std::set<storm::expressions::Variable> containedVariables = variable.getLowerBoundExpression().getVariables();
1408 std::set<storm::expressions::Variable> illegalVariables;
1409 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1410 std::inserter(illegalVariables, illegalVariables.begin()));
1411 bool isValid = illegalVariables.empty();
1413 std::vector<std::string> illegalVariableNames;
1414 for (
auto const& var : illegalVariables) {
1415 illegalVariableNames.push_back(var.getName());
1418 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1419 <<
": lower bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1424 if (variable.hasUpperBoundExpression()) {
1425 std::set<storm::expressions::Variable> containedVariables = variable.getUpperBoundExpression().getVariables();
1426 std::set<storm::expressions::Variable> illegalVariables;
1428 illegalVariables.clear();
1429 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1430 std::inserter(illegalVariables, illegalVariables.begin()));
1431 bool isValid = illegalVariables.empty();
1433 std::vector<std::string> illegalVariableNames;
1434 for (
auto const& var : illegalVariables) {
1435 illegalVariableNames.push_back(var.getName());
1438 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1439 <<
": upper bound expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",")
1444 if (variable.hasInitialValue()) {
1445 STORM_LOG_THROW(!this->hasInitialConstruct(), storm::exceptions::WrongFormatException,
1446 "Error for " << module.getName() <<
"." << variable.getName() <<
" (" << variable.getFilename() <<
", line "
1447 << variable.getLineNumber() <<
"): illegal to specify initial value if an initial construct is present.");
1450 std::set<storm::expressions::Variable> containedVariables = variable.getInitialValueExpression().getVariables();
1451 std::set<storm::expressions::Variable> illegalVariables;
1452 illegalVariables.clear();
1453 std::set_difference(containedVariables.begin(), containedVariables.end(), constants.begin(), constants.end(),
1454 std::inserter(illegalVariables, illegalVariables.begin()));
1455 bool isValid = illegalVariables.empty();
1457 std::vector<std::string> illegalVariableNames;
1458 for (
auto const& var : illegalVariables) {
1459 illegalVariableNames.push_back(var.getName());
1462 isValid, storm::exceptions::WrongFormatException,
1463 "Error in " << variable.getFilename() <<
", line " << variable.getLineNumber()
1464 <<
": initial value expression refers to unknown constants: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1469 variables.insert(variable.getExpressionVariable());
1470 all.insert(variable.getExpressionVariable());
1473 for (
auto const& variable : module.getClockVariables()) {
1475 variables.insert(variable.getExpressionVariable());
1476 all.insert(variable.getExpressionVariable());
1481 std::set<storm::expressions::Variable> variablesAndConstants;
1482 std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
1485 for (
auto const& formula : this->getFormulas()) {
1486 std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
1487 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1489 "Error in " << formula.getFilename() <<
", line " << formula.getLineNumber() <<
": expression '" << formula.getExpression()
1490 <<
"'of formula '" << formula.getName() <<
"' refers to unknown identifiers.");
1491 if (formula.hasExpressionVariable()) {
1492 all.insert(formula.getExpressionVariable());
1493 variablesAndConstants.insert(formula.getExpressionVariable());
1498 bool hasProbabilisticCommand =
false;
1499 bool hasMarkovianCommand =
false;
1500 bool hasLabeledMarkovianCommand =
false;
1501 std::map<std::pair<storm::expressions::Variable, uint64_t>, std::pair<uint64_t, std::string>> writtenGlobalVariables;
1502 for (
auto const& module : this->getModules()) {
1503 std::set<storm::expressions::Variable> legalVariables = globalVariables;
1504 for (
auto const& variable : module.getBooleanVariables()) {
1505 legalVariables.insert(variable.getExpressionVariable());
1507 for (
auto const& variable : module.getIntegerVariables()) {
1508 legalVariables.insert(variable.getExpressionVariable());
1510 for (
auto const& variable : module.getClockVariables()) {
1511 legalVariables.insert(variable.getExpressionVariable());
1514 if (module.hasInvariant()) {
1515 std::set<storm::expressions::Variable> containedVariables =
module.getInvariant().getVariables();
1516 std::set<storm::expressions::Variable> illegalVariables;
1517 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1518 std::inserter(illegalVariables, illegalVariables.begin()));
1519 bool isValid = illegalVariables.empty();
1521 std::vector<std::string> illegalVariableNames;
1522 for (
auto const& var : illegalVariables) {
1523 illegalVariableNames.push_back(var.getName());
1526 "Error in " << module.getFilename() <<
", line " << module.getLineNumber() <<
": invariant " << module.getInvariant()
1527 <<
" refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1529 STORM_LOG_THROW(module.getInvariant().hasBooleanType(), storm::exceptions::WrongFormatException,
1530 "Error in " << module.getFilename() <<
", line " << module.getLineNumber() <<
": invariant " << module.getInvariant()
1531 <<
" must evaluate to type 'bool'.");
1534 for (
auto& command : module.getCommands()) {
1536 std::set<storm::expressions::Variable> containedVariables = command.getGuardExpression().getVariables();
1537 std::set<storm::expressions::Variable> illegalVariables;
1538 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1539 std::inserter(illegalVariables, illegalVariables.begin()));
1540 bool isValid = illegalVariables.empty();
1542 std::vector<std::string> illegalVariableNames;
1543 for (
auto const& var : illegalVariables) {
1544 illegalVariableNames.push_back(var.getName());
1547 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": guard " << command.getGuardExpression()
1548 <<
" refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1551 command.getGuardExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1552 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": expression for guard must evaluate to type 'bool'.");
1555 if (command.isMarkovian()) {
1556 hasMarkovianCommand =
true;
1558 hasProbabilisticCommand =
true;
1563 if (command.isMarkovian() && command.isLabeled()) {
1564 hasLabeledMarkovianCommand =
true;
1568 for (
auto const& update : command.getUpdates()) {
1569 containedVariables.clear();
1570 if (update.isLikelihoodInterval()) {
1571 update.getLikelihoodExpressionInterval().first.gatherVariables(containedVariables);
1572 update.getLikelihoodExpressionInterval().second.gatherVariables(containedVariables);
1574 update.getLikelihoodExpression().gatherVariables(containedVariables);
1576 illegalVariables.clear();
1577 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1578 std::inserter(illegalVariables, illegalVariables.begin()));
1579 isValid = illegalVariables.empty();
1581 std::vector<std::string> illegalVariableNames;
1582 for (
auto const& var : illegalVariables) {
1583 illegalVariableNames.push_back(var.getName());
1586 isValid, storm::exceptions::WrongFormatException,
1587 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1588 <<
": likelihood expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1592 std::set<storm::expressions::Variable> alreadyAssignedVariables;
1593 for (
auto const& assignment : update.getAssignments()) {
1596 if (legalVariables.find(assignedVariable) == legalVariables.end()) {
1597 if (all.find(assignedVariable) != all.end()) {
1599 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1600 <<
": assignment illegally refers to variable '" << assignment.getVariableName() <<
"'.");
1603 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1604 <<
": assignment refers to unknown variable '" << assignment.getVariableName() <<
"'.");
1607 STORM_LOG_THROW(alreadyAssignedVariables.find(assignedVariable) == alreadyAssignedVariables.end(), storm::exceptions::WrongFormatException,
1608 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": duplicate assignment to variable '"
1609 << assignment.getVariableName() <<
"'.");
1611 (assignedVariable.
getType().
isRationalType() && assignment.getExpression().getType().isNumericalType()),
1612 storm::exceptions::WrongFormatException,
1613 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": illegally assigning a value of type '"
1614 << assignment.getExpression().getType() <<
"' to variable '" << assignment.getVariableName() <<
"' of type '"
1615 << assignedVariable.
getType() <<
"'.");
1617 if (command.isLabeled() && globalVariables.find(assignedVariable) != globalVariables.end()) {
1618 std::pair<storm::expressions::Variable, uint64_t> variableActionIndexPair(assignedVariable, command.getActionIndex());
1619 std::pair<uint64_t, std::string> lineModuleNamePair(command.getLineNumber(), module.getName());
1620 auto insertionResult = writtenGlobalVariables.emplace(variableActionIndexPair, lineModuleNamePair);
1622 insertionResult.second || insertionResult.first->second.second == module.getName(), storm::exceptions::WrongFormatException,
1623 "Error in " << command.getFilename() <<
", line " << command.getLineNumber() <<
": Syncronizing command with action label '"
1624 << command.getActionName() <<
"' illegally assigns a value to global variable '" << assignedVariable.
getName()
1625 <<
"'. Previous assignment to the variable at line " << insertionResult.first->second.first <<
" in module '"
1626 << insertionResult.first->second.second <<
"'.");
1629 containedVariables = assignment.getExpression().getVariables();
1630 illegalVariables.clear();
1631 std::set_difference(containedVariables.begin(), containedVariables.end(), variablesAndConstants.begin(), variablesAndConstants.end(),
1632 std::inserter(illegalVariables, illegalVariables.begin()));
1633 isValid = illegalVariables.empty();
1635 std::vector<std::string> illegalVariableNames;
1636 for (
auto const& var : illegalVariables) {
1637 illegalVariableNames.push_back(var.getName());
1640 isValid, storm::exceptions::WrongFormatException,
1641 "Error in " << command.getFilename() <<
", line " << command.getLineNumber()
1642 <<
": assigned expression refers to unknown identifiers: " << boost::algorithm::join(illegalVariableNames,
",") <<
".");
1646 alreadyAssignedVariables.insert(assignedVariable);
1652 if (hasLabeledMarkovianCommand) {
1653 if (prismCompatibility) {
1655 false,
"The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1658 "The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.");
1663 STORM_LOG_THROW(!hasMarkovianCommand, storm::exceptions::WrongFormatException,
"Discrete-time model must not have Markovian commands.");
1664 }
else if (this->
getModelType() == Program::ModelType::CTMC) {
1665 STORM_LOG_THROW(!hasProbabilisticCommand, storm::exceptions::WrongFormatException,
1666 "The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Please use Markovian commands instead or turn "
1667 "on the PRISM compatibility mode using the flag '-pc'.");
1671 for (
auto const& rewardModel : this->getRewardModels()) {
1672 for (
auto const& stateReward : rewardModel.getStateRewards()) {
1673 std::set<storm::expressions::Variable> containedVariables = stateReward.getStatePredicateExpression().getVariables();
1674 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1676 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber()
1677 <<
": state reward expression refers to unknown identifiers.");
1679 stateReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1680 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber() <<
": state predicate must evaluate to type 'bool'.");
1682 containedVariables = stateReward.getRewardValueExpression().getVariables();
1683 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1685 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber()
1686 <<
": state reward value expression refers to unknown identifiers.");
1687 STORM_LOG_THROW(stateReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1688 "Error in " << stateReward.getFilename() <<
", line " << stateReward.getLineNumber()
1689 <<
": reward value expression must evaluate to numerical type.");
1692 for (
auto const& stateActionReward : rewardModel.getStateActionRewards()) {
1693 std::set<storm::expressions::Variable> containedVariables = stateActionReward.getStatePredicateExpression().getVariables();
1694 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1696 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1697 <<
": state reward expression refers to unknown identifiers.");
1698 STORM_LOG_THROW(stateActionReward.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1699 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1700 <<
": state predicate must evaluate to type 'bool'.");
1702 containedVariables = stateActionReward.getRewardValueExpression().getVariables();
1703 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1705 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1706 <<
": state reward value expression refers to unknown identifiers.");
1707 STORM_LOG_THROW(stateActionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1708 "Error in " << stateActionReward.getFilename() <<
", line " << stateActionReward.getLineNumber()
1709 <<
": reward value expression must evaluate to numerical type.");
1712 for (
auto const& transitionReward : rewardModel.getTransitionRewards()) {
1713 std::set<storm::expressions::Variable> containedVariables = transitionReward.getSourceStatePredicateExpression().getVariables();
1714 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1716 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1717 <<
": state reward expression refers to unknown identifiers.");
1718 STORM_LOG_THROW(transitionReward.getSourceStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1719 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1720 <<
": state predicate must evaluate to type 'bool'.");
1722 containedVariables = transitionReward.getTargetStatePredicateExpression().getVariables();
1723 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1725 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1726 <<
": state reward expression refers to unknown identifiers.");
1727 STORM_LOG_THROW(transitionReward.getTargetStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1728 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1729 <<
": state predicate must evaluate to type 'bool'.");
1731 containedVariables = transitionReward.getRewardValueExpression().getVariables();
1732 isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1734 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1735 <<
": state reward value expression refers to unknown identifiers.");
1736 STORM_LOG_THROW(transitionReward.getRewardValueExpression().hasNumericalType(), storm::exceptions::WrongFormatException,
1737 "Error in " << transitionReward.getFilename() <<
", line " << transitionReward.getLineNumber()
1738 <<
": reward value expression must evaluate to numerical type.");
1743 if (this->hasInitialConstruct()) {
1744 std::set<storm::expressions::Variable> containedIdentifiers = this->getInitialConstruct().getInitialStatesExpression().getVariables();
1745 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
1747 "Error in " << this->getInitialConstruct().getFilename() <<
", line " << this->getInitialConstruct().getLineNumber()
1748 <<
": initial construct refers to unknown identifiers.");
1752 if (systemCompositionConstruct) {
1753 CompositionValidityChecker checker(*
this);
1754 checker.check(systemCompositionConstruct.get().getSystemComposition());
1758 for (
auto const& label : this->getLabels()) {
1759 std::set<storm::expressions::Variable> containedVariables = label.getStatePredicateExpression().getVariables();
1760 bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
1762 "Error in " << label.getFilename() <<
", line " << label.getLineNumber() <<
": label expression refers to unknown identifiers.");
1763 STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException,
1764 "Error in " << label.getFilename() <<
", line " << label.getLineNumber() <<
": label predicate must evaluate to type 'bool'.");
1768 for (
auto const& player : this->getPlayers()) {
1770 for (
auto const& controlledAction : player.getActions()) {
1771 STORM_LOG_THROW(this->hasAction(controlledAction), storm::exceptions::InternalException,
1772 "Error in " << player.getFilename() <<
", line " << player.getLineNumber() <<
": The player controlled action " << controlledAction
1773 <<
" is not available.");
1775 for (
auto const& controlledModule : player.getModules()) {
1777 "Error in " << player.getFilename() <<
", line " << player.getLineNumber() <<
": The player controlled module " << controlledModule
1778 <<
" is not available.");
1782 if (lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
1784 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;
1785 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommand;
1786 for (
auto const& module : this->getModules()) {
1787 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommandInThisModule;
1788 std::set<std::pair<std::string, std::string>> globalIVarsWrittenToByCommandInThisModule;
1789 for (
auto const& command : module.getCommands()) {
1790 if (!command.isLabeled())
1792 for (
auto const& update : command.getUpdates()) {
1793 for (
auto const& assignment : update.getAssignments()) {
1794 if (this->globalBooleanVariableExists(assignment.getVariable().getName())) {
1795 globalBVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1796 }
else if (this->globalIntegerVariableExists(assignment.getVariable().getName())) {
1797 globalIVarsWrittenToByCommandInThisModule.insert({assignment.getVariable().getName(), command.getActionName()});
1802 for (
auto const& entry : globalIVarsWrittenToByCommandInThisModule) {
1803 if (globalIVarsWrittenToByCommand.find(entry) != globalIVarsWrittenToByCommand.end()) {
1805 "Error in " << module.getFilename() <<
", line " << module.getLineNumber()
1806 <<
": assignment of (possibly) synchronizing command with label '" << entry.second
1807 <<
"' writes to global variable '" << entry.first <<
"'.");
1810 for (
auto const& entry : globalBVarsWrittenToByCommandInThisModule) {
1811 if (globalBVarsWrittenToByCommand.find(entry) != globalBVarsWrittenToByCommand.end()) {
1813 "Error in " << module.getFilename() <<
", line " << module.getLineNumber()
1814 <<
": assignment of (possibly) synchronizing command with label '" << entry.second
1815 <<
"' writes to global variable '" << entry.first <<
"'.");
1970Program Program::flattenModules(std::shared_ptr<storm::utility::solver::SmtSolverFactory>
const& smtSolverFactory)
const {
1972 if (this->getNumberOfModules() == 1) {
1976 STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException,
1977 "Unable to flatten modules for model of type '" << this->getModelType() <<
"'.");
1982 std::unique_ptr<storm::solver::SmtSolver> solver = smtSolverFactory->create(*manager);
1985 std::stringstream newModuleName;
1986 std::vector<storm::prism::BooleanVariable> allBooleanVariables;
1987 std::vector<storm::prism::IntegerVariable> allIntegerVariables;
1988 std::vector<storm::prism::ClockVariable> allClockVariables;
1989 std::vector<storm::prism::Command> newCommands;
1990 uint_fast64_t nextCommandIndex = 0;
1991 uint_fast64_t nextUpdateIndex = 0;
1994 for (
auto const& constant : this->getConstants()) {
1995 if (constant.isDefined()) {
1996 if (constant.getType().isBooleanType()) {
1999 solver->add(constant.getExpressionVariable() == constant.getExpression());
2005 for (
auto const& variable : this->getGlobalIntegerVariables()) {
2006 solver->add(variable.getRangeExpression());
2011 allBooleanVariables.insert(allBooleanVariables.end(), this->getGlobalBooleanVariables().begin(), this->getGlobalBooleanVariables().end());
2012 allIntegerVariables.insert(allIntegerVariables.end(), this->getGlobalIntegerVariables().begin(), this->getGlobalIntegerVariables().end());
2017 for (
auto const& module : this->getModules()) {
2018 newModuleName <<
module.getName() << "_";
2019 allBooleanVariables.insert(allBooleanVariables.end(),
module.getBooleanVariables().begin(), module.getBooleanVariables().end());
2020 allIntegerVariables.insert(allIntegerVariables.end(), module.getIntegerVariables().begin(), module.getIntegerVariables().end());
2021 allClockVariables.insert(allClockVariables.end(), module.getClockVariables().begin(), module.getClockVariables().end());
2023 for (
auto const& variable :
module.getIntegerVariables()) {
2024 solver->add(variable.getRangeExpression());
2027 if (module.hasInvariant()) {
2028 newInvariant = newInvariant.
isInitialized() ? (newInvariant &&
module.getInvariant()) : module.getInvariant();
2033 for (
auto const& command :
module.getCommands()) {
2034 if (!command.isLabeled()) {
2035 std::vector<storm::prism::Update> updates;
2036 updates.reserve(command.getUpdates().size());
2038 for (
auto const& update : command.getUpdates()) {
2040 storm::prism::Update(nextUpdateIndex, update.getLikelihoodExpression(), update.getAssignments(), update.getFilename(), 0));
2044 newCommands.push_back(
storm::prism::Command(nextCommandIndex, command.isMarkovian(), actionToIndexMap.find(
"")->second,
"",
2045 command.getGuardExpression(), updates, command.getFilename(), 0));
2057 for (
auto const& actionIndex : this->getSynchronizingActionIndices()) {
2058 bool noCombinationsForAction =
false;
2061 std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>> possibleCommands;
2063 for (
auto const& module : this->getModules()) {
2065 if (!module.hasActionIndex(actionIndex)) {
2069 std::set<uint_fast64_t>
const& commandIndices =
module.getCommandIndicesByActionIndex(actionIndex);
2073 if (commandIndices.empty()) {
2074 noCombinationsForAction =
true;
2079 possibleCommands.push_back(std::vector<std::reference_wrapper<storm::prism::Command const>>());
2082 for (
auto const& commandIndex : commandIndices) {
2083 possibleCommands.back().push_back(module.getCommand(commandIndex));
2089 if (!noCombinationsForAction) {
2094 std::vector<std::vector<storm::expressions::Variable>> commandVariables(possibleCommands.size());
2095 std::vector<storm::expressions::Variable> allCommandVariables;
2096 for (uint_fast64_t outerIndex = 0; outerIndex < possibleCommands.size(); ++outerIndex) {
2098 for (uint_fast64_t innerIndex = 0; innerIndex < possibleCommands[outerIndex].size(); ++innerIndex) {
2099 commandVariables[outerIndex].push_back(
manager->declareFreshBooleanVariable());
2100 allCommandVariables.push_back(commandVariables[outerIndex].back());
2101 solver->add(
implies(commandVariables[outerIndex].back(), possibleCommands[outerIndex][innerIndex].get().getGuardExpression()));
2105 for (
auto const& commandVariable : commandVariables[outerIndex]) {
2106 atLeastOneCommandFromModule = atLeastOneCommandFromModule || commandVariable;
2108 solver->add(atLeastOneCommandFromModule);
2117 std::vector<std::vector<std::reference_wrapper<Command const>>> chosenCommands(possibleCommands.size());
2119 for (uint_fast64_t outerIndex = 0; outerIndex < commandVariables.size(); ++outerIndex) {
2120 for (uint_fast64_t innerIndex = 0; innerIndex < commandVariables[outerIndex].size(); ++innerIndex) {
2121 if (modelReference.
getBooleanValue(commandVariables[outerIndex][innerIndex])) {
2122 chosenCommands[outerIndex].push_back(possibleCommands[outerIndex][innerIndex]);
2129 std::vector<std::vector<std::reference_wrapper<Command const>>::const_iterator> iterators;
2130 for (
auto const& element : chosenCommands) {
2131 iterators.push_back(element.begin());
2134 bool movedAtLeastOneIterator =
false;
2135 std::vector<std::reference_wrapper<Command const>> commandCombination(chosenCommands.size(), chosenCommands.front().front());
2136 std::vector<uint_fast64_t> commandCombinationIndices(iterators.size());
2138 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2139 commandCombination[index] = *iterators[index];
2140 commandCombinationIndices[index] = commandCombination[index].get().getGlobalIndex();
2144 auto seenIt = seenCommandCombinations.find(commandCombinationIndices);
2145 if (seenIt == seenCommandCombinations.end()) {
2146 newCommands.push_back(synchronizeCommands(nextCommandIndex, actionIndex, nextUpdateIndex, indexToActionMap.find(actionIndex)->second,
2147 commandCombination));
2148 seenCommandCombinations.insert(commandCombinationIndices);
2152 nextUpdateIndex += newCommands.back().getNumberOfUpdates();
2155 movedAtLeastOneIterator =
false;
2156 for (uint_fast64_t index = 0; index < iterators.size(); ++index) {
2158 if (iterators[index] != chosenCommands[index].cend()) {
2159 movedAtLeastOneIterator =
true;
2162 iterators[index] = chosenCommands[index].cbegin();
2165 }
while (movedAtLeastOneIterator);
2175 storm::prism::Module singleModule(newModuleName.str(), allBooleanVariables, allIntegerVariables, allClockVariables, newInvariant, newCommands,
2176 this->getFilename(), 0);
2178 return Program(manager, this->
getModelType(), this->getConstants(), std::vector<storm::prism::BooleanVariable>(),
2179 std::vector<storm::prism::IntegerVariable>(), this->getFormulas(), this->getPlayers(), {singleModule}, actionToIndexMap,
2180 this->getRewardModels(), this->getLabels(), this->getObservationLabels(), this->getOptionalInitialConstruct(),
2181 this->getOptionalSystemCompositionConstruct(), prismCompatibility, this->getFilename(), 0,
true);