12#ifndef MCRL2_CORE_DETAIL_SOUNDNESS_CHECKS_H
13#define MCRL2_CORE_DETAIL_SOUNDNESS_CHECKS_H
18#include "mcrl2/atermpp/concepts.h"
19#include "mcrl2/atermpp/aterm_string.h"
20#include "mcrl2/core/detail/function_symbols.h"
27template <atermpp::IsATerm Term,
typename CheckFunction>
37template <atermpp::IsATerm Term,
typename CheckFunction>
41 if (!t.type_is_list())
45 const atermpp::aterm_list& l = atermpp::down_cast<atermpp::aterm_list>(term);
46 if (l.size() < minimum_size)
50 for (
const auto& x: l)
60template <atermpp::IsATerm Term>
64 if (!term.type_is_appl())
79template <atermpp::IsATerm Term>
83 if (!term.type_is_appl())
87 return term.size() <= 0;
90template <atermpp::IsATerm Term>
94 return term.type_is_int();
100template <atermpp::IsATerm Term>
103#ifndef MCRL2_NO_SOUNDNESS_CHECKS
106 if (term.type_is_int())
110 if (!term.type_is_appl())
118#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
119 for (
const atermpp::aterm& child : term)
121 if (!check_term_argument(child, check_rule_DataExpr<atermpp::aterm>))
123 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
212template <atermpp::IsATerm Term>
bool check_term_Whr(
const Term& t);
240template <atermpp::IsATerm Term>
bool check_term_Tau(
const Term& t);
241template <atermpp::IsATerm Term>
bool check_term_Sum(
const Term& t);
249template <atermpp::IsATerm Term>
bool check_term_Seq(
const Term& t);
320template <atermpp::IsATerm Term>
bool check_term_Mu(
const Term& t);
321template <atermpp::IsATerm Term>
bool check_term_Nu(
const Term& t);
353template <atermpp::IsATerm Term>
356#ifndef MCRL2_NO_SOUNDNESS_CHECKS
357 return check_rule_SortId(t)
358 || check_term_SortCons(t)
359 || check_term_SortStruct(t)
360 || check_term_SortArrow(t)
361 || check_term_UntypedSortUnknown(t)
362 || check_term_UntypedSortsPossible(t)
363 || check_term_UntypedSortVariable(t);
369template <atermpp::IsATerm Term>
372#ifndef MCRL2_NO_SOUNDNESS_CHECKS
373 return check_term_SortId(t);
379template <atermpp::IsATerm Term>
382#ifndef MCRL2_NO_SOUNDNESS_CHECKS
383 return check_term_SortList(t)
384 || check_term_SortSet(t)
385 || check_term_SortBag(t)
386 || check_term_SortFSet(t)
387 || check_term_SortFBag(t);
393template <atermpp::IsATerm Term>
396#ifndef MCRL2_NO_SOUNDNESS_CHECKS
397 return check_term_StructCons(t);
403template <atermpp::IsATerm Term>
406#ifndef MCRL2_NO_SOUNDNESS_CHECKS
407 return check_term_StructProj(t);
413template <atermpp::IsATerm Term>
416#ifndef MCRL2_NO_SOUNDNESS_CHECKS
417 return check_rule_DataVarId(t)
418 || check_rule_OpId(t)
419 || check_term_DataAppl(t)
420 || check_term_Binder(t)
422 || check_term_UntypedIdentifier(t);
428template <atermpp::IsATerm Term>
431#ifndef MCRL2_NO_SOUNDNESS_CHECKS
432 return check_term_DataVarId(t);
438template <atermpp::IsATerm Term>
441#ifndef MCRL2_NO_SOUNDNESS_CHECKS
442 return check_term_OpId(t);
448template <atermpp::IsATerm Term>
451#ifndef MCRL2_NO_SOUNDNESS_CHECKS
452 return check_term_UntypedDataParameter(t);
458template <atermpp::IsATerm Term>
461#ifndef MCRL2_NO_SOUNDNESS_CHECKS
462 return check_term_Forall(t)
463 || check_term_Exists(t)
464 || check_term_SetComp(t)
465 || check_term_BagComp(t)
466 || check_term_Lambda(t)
467 || check_term_UntypedSetBagComp(t);
473template <atermpp::IsATerm Term>
476#ifndef MCRL2_NO_SOUNDNESS_CHECKS
477 return check_rule_DataVarIdInit(t)
478 || check_rule_UntypedIdentifierAssignment(t);
484template <atermpp::IsATerm Term>
487#ifndef MCRL2_NO_SOUNDNESS_CHECKS
488 return check_term_DataVarIdInit(t);
494template <atermpp::IsATerm Term>
497#ifndef MCRL2_NO_SOUNDNESS_CHECKS
498 return check_term_UntypedIdentifierAssignment(t);
504template <atermpp::IsATerm Term>
507#ifndef MCRL2_NO_SOUNDNESS_CHECKS
508 return check_term_DataSpec(t);
514template <atermpp::IsATerm Term>
517#ifndef MCRL2_NO_SOUNDNESS_CHECKS
518 return check_term_SortSpec(t);
524template <atermpp::IsATerm Term>
527#ifndef MCRL2_NO_SOUNDNESS_CHECKS
528 return check_term_ConsSpec(t);
534template <atermpp::IsATerm Term>
537#ifndef MCRL2_NO_SOUNDNESS_CHECKS
538 return check_term_MapSpec(t);
544template <atermpp::IsATerm Term>
547#ifndef MCRL2_NO_SOUNDNESS_CHECKS
548 return check_term_DataEqnSpec(t);
554template <atermpp::IsATerm Term>
557#ifndef MCRL2_NO_SOUNDNESS_CHECKS
558 return check_rule_SortId(t)
559 || check_term_SortRef(t);
565template <atermpp::IsATerm Term>
568#ifndef MCRL2_NO_SOUNDNESS_CHECKS
569 return check_term_DataEqn(t);
575template <atermpp::IsATerm Term>
578#ifndef MCRL2_NO_SOUNDNESS_CHECKS
579 return check_term_MultAct(t);
585template <atermpp::IsATerm Term>
588#ifndef MCRL2_NO_SOUNDNESS_CHECKS
589 return check_term_TimedMultAct(t);
595template <atermpp::IsATerm Term>
598#ifndef MCRL2_NO_SOUNDNESS_CHECKS
599 return check_term_UntypedMultiAction(t);
605template <atermpp::IsATerm Term>
608#ifndef MCRL2_NO_SOUNDNESS_CHECKS
609 return check_term_Action(t);
615template <atermpp::IsATerm Term>
618#ifndef MCRL2_NO_SOUNDNESS_CHECKS
619 return check_term_ActId(t);
625template <atermpp::IsATerm Term>
628#ifndef MCRL2_NO_SOUNDNESS_CHECKS
629 return check_rule_Action(t)
630 || check_term_Process(t)
631 || check_term_ProcessAssignment(t)
632 || check_term_Delta(t)
635 || check_term_Block(t)
636 || check_term_Hide(t)
637 || check_term_Rename(t)
638 || check_term_Comm(t)
639 || check_term_Allow(t)
640 || check_term_Sync(t)
641 || check_term_AtTime(t)
643 || check_term_IfThen(t)
644 || check_term_IfThenElse(t)
645 || check_term_BInit(t)
646 || check_term_Merge(t)
647 || check_term_LMerge(t)
648 || check_term_Choice(t)
649 || check_term_StochasticOperator(t)
650 || check_term_UntypedProcessAssignment(t)
651 || check_rule_UntypedDataParameter(t);
657template <atermpp::IsATerm Term>
660#ifndef MCRL2_NO_SOUNDNESS_CHECKS
661 return check_term_ProcVarId(t);
667template <atermpp::IsATerm Term>
670#ifndef MCRL2_NO_SOUNDNESS_CHECKS
671 return check_term_MultActName(t);
677template <atermpp::IsATerm Term>
680#ifndef MCRL2_NO_SOUNDNESS_CHECKS
681 return check_term_RenameExpr(t);
687template <atermpp::IsATerm Term>
690#ifndef MCRL2_NO_SOUNDNESS_CHECKS
691 return check_term_CommExpr(t);
697template <atermpp::IsATerm Term>
700#ifndef MCRL2_NO_SOUNDNESS_CHECKS
701 return check_term_ProcSpec(t);
707template <atermpp::IsATerm Term>
710#ifndef MCRL2_NO_SOUNDNESS_CHECKS
711 return check_term_ActSpec(t);
717template <atermpp::IsATerm Term>
720#ifndef MCRL2_NO_SOUNDNESS_CHECKS
721 return check_term_GlobVarSpec(t);
727template <atermpp::IsATerm Term>
730#ifndef MCRL2_NO_SOUNDNESS_CHECKS
731 return check_term_ProcEqnSpec(t);
737template <atermpp::IsATerm Term>
740#ifndef MCRL2_NO_SOUNDNESS_CHECKS
741 return check_term_ProcEqn(t);
747template <atermpp::IsATerm Term>
750#ifndef MCRL2_NO_SOUNDNESS_CHECKS
751 return check_rule_MultAct(t)
752 || check_term_Delta(t);
758template <atermpp::IsATerm Term>
761#ifndef MCRL2_NO_SOUNDNESS_CHECKS
762 return check_term_ProcessInit(t);
768template <atermpp::IsATerm Term>
771#ifndef MCRL2_NO_SOUNDNESS_CHECKS
772 return check_term_Distribution(t);
778template <atermpp::IsATerm Term>
781#ifndef MCRL2_NO_SOUNDNESS_CHECKS
782 return check_term_LinProcSpec(t);
788template <atermpp::IsATerm Term>
791#ifndef MCRL2_NO_SOUNDNESS_CHECKS
792 return check_term_LinearProcess(t);
798template <atermpp::IsATerm Term>
801#ifndef MCRL2_NO_SOUNDNESS_CHECKS
802 return check_term_LinearProcessSummand(t);
808template <atermpp::IsATerm Term>
811#ifndef MCRL2_NO_SOUNDNESS_CHECKS
812 return check_term_LinearProcessInit(t);
818template <atermpp::IsATerm Term>
821#ifndef MCRL2_NO_SOUNDNESS_CHECKS
822 return check_rule_DataExpr(t)
823 || check_term_StateTrue(t)
824 || check_term_StateFalse(t)
825 || check_term_StateNot(t)
826 || check_term_StateMinus(t)
827 || check_term_StateAnd(t)
828 || check_term_StateOr(t)
829 || check_term_StateImp(t)
830 || check_term_StatePlus(t)
831 || check_term_StateConstantMultiply(t)
832 || check_term_StateConstantMultiplyAlt(t)
833 || check_term_StateForall(t)
834 || check_term_StateExists(t)
835 || check_term_StateInfimum(t)
836 || check_term_StateSupremum(t)
837 || check_term_StateSum(t)
838 || check_term_StateMust(t)
839 || check_term_StateMay(t)
840 || check_term_StateYaled(t)
841 || check_term_StateYaledTimed(t)
842 || check_term_StateDelay(t)
843 || check_term_StateDelayTimed(t)
844 || check_term_StateVar(t)
845 || check_term_StateNu(t)
846 || check_term_StateMu(t)
847 || check_rule_UntypedDataParameter(t);
853template <atermpp::IsATerm Term>
856#ifndef MCRL2_NO_SOUNDNESS_CHECKS
857 return check_rule_ActFrm(t)
858 || check_term_RegNil(t)
859 || check_term_RegSeq(t)
860 || check_term_RegAlt(t)
861 || check_term_RegTrans(t)
862 || check_term_RegTransOrNil(t)
863 || check_term_UntypedRegFrm(t);
869template <atermpp::IsATerm Term>
872#ifndef MCRL2_NO_SOUNDNESS_CHECKS
873 return check_rule_DataExpr(t)
874 || check_term_ActTrue(t)
875 || check_term_ActFalse(t)
876 || check_term_ActNot(t)
877 || check_term_ActAnd(t)
878 || check_term_ActOr(t)
879 || check_term_ActImp(t)
880 || check_term_ActForall(t)
881 || check_term_ActExists(t)
882 || check_term_ActAt(t)
883 || check_term_ActMultAct(t)
884 || check_rule_UntypedDataParameter(t)
885 || check_rule_UntypedMultiAction(t);
891template <atermpp::IsATerm Term>
894#ifndef MCRL2_NO_SOUNDNESS_CHECKS
895 return check_rule_UntypedDataParameter(t)
896 || check_rule_Action(t);
902template <atermpp::IsATerm Term>
905#ifndef MCRL2_NO_SOUNDNESS_CHECKS
906 return check_term_ActionRenameRules(t);
912template <atermpp::IsATerm Term>
915#ifndef MCRL2_NO_SOUNDNESS_CHECKS
916 return check_term_ActionRenameRule(t);
922template <atermpp::IsATerm Term>
925#ifndef MCRL2_NO_SOUNDNESS_CHECKS
926 return check_rule_UntypedDataParameter(t)
927 || check_rule_Action(t)
928 || check_term_Delta(t)
929 || check_term_Tau(t);
935template <atermpp::IsATerm Term>
938#ifndef MCRL2_NO_SOUNDNESS_CHECKS
939 return check_term_ActionRenameSpec(t);
945template <atermpp::IsATerm Term>
948#ifndef MCRL2_NO_SOUNDNESS_CHECKS
949 return check_term_PBES(t);
955template <atermpp::IsATerm Term>
958#ifndef MCRL2_NO_SOUNDNESS_CHECKS
959 return check_term_PBEqnSpec(t);
965template <atermpp::IsATerm Term>
968#ifndef MCRL2_NO_SOUNDNESS_CHECKS
969 return check_term_PBInit(t);
975template <atermpp::IsATerm Term>
978#ifndef MCRL2_NO_SOUNDNESS_CHECKS
979 return check_term_PBEqn(t);
985template <atermpp::IsATerm Term>
988#ifndef MCRL2_NO_SOUNDNESS_CHECKS
989 return check_term_Mu(t)
996template <atermpp::IsATerm Term>
999#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1000 return check_term_PropVarDecl(t);
1006template <atermpp::IsATerm Term>
1009#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1010 return check_rule_DataExpr(t)
1011 || check_term_PBESTrue(t)
1012 || check_term_PBESFalse(t)
1013 || check_term_PBESNot(t)
1014 || check_term_PBESAnd(t)
1015 || check_term_PBESOr(t)
1016 || check_term_PBESImp(t)
1017 || check_term_PBESForall(t)
1018 || check_term_PBESExists(t)
1019 || check_rule_PropVarInst(t)
1020 || check_rule_UntypedDataParameter(t);
1026template <atermpp::IsATerm Term>
1029#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1030 return check_term_PropVarInst(t);
1036template <atermpp::IsATerm Term>
1039#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1040 return check_term_PRES(t);
1046template <atermpp::IsATerm Term>
1049#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1050 return check_term_PREqnSpec(t);
1056template <atermpp::IsATerm Term>
1059#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1060 return check_term_PRInit(t);
1066template <atermpp::IsATerm Term>
1069#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1070 return check_term_PREqn(t);
1076template <atermpp::IsATerm Term>
1079#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1080 return check_rule_DataExpr(t)
1081 || check_term_PRESTrue(t)
1082 || check_term_PRESFalse(t)
1083 || check_term_PRESMinus(t)
1084 || check_term_PRESAnd(t)
1085 || check_term_PRESOr(t)
1086 || check_term_PRESImp(t)
1087 || check_term_PRESPlus(t)
1088 || check_term_PRESConstantMultiply(t)
1089 || check_term_PRESConstantMultiplyAlt(t)
1090 || check_term_PRESInfimum(t)
1091 || check_term_PRESSupremum(t)
1092 || check_term_PRESSum(t)
1093 || check_term_PRESEqInf(t)
1094 || check_term_PRESEqNInf(t)
1095 || check_term_PRESCondSm(t)
1096 || check_term_PRESCondEq(t)
1097 || check_rule_PropVarInst(t)
1098 || check_rule_UntypedDataParameter(t);
1105template <atermpp::IsATerm Term>
1108#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1111 if (!term.type_is_appl())
1115 if (term.function() != core::detail::function_symbols::SortCons)
1121 if (term.size() != 2)
1125#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1126 if (!check_term_argument(term[0], check_rule_SortConsType<atermpp::aterm>))
1128 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortConsType" << std::endl;
1131 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1133 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
1143template <atermpp::IsATerm Term>
1146#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1149 if (!term.type_is_appl())
1153 if (term.function() != core::detail::function_symbols::SortStruct)
1159 if (term.size() != 1)
1163#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1164 if (!check_list_argument(term[0], check_rule_StructCons<atermpp::aterm>, 1))
1166 mCRL2log(log::log_level_t::debug) <<
"check_rule_StructCons" << std::endl;
1176template <atermpp::IsATerm Term>
1179#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1182 if (!term.type_is_appl())
1186 if (term.function() != core::detail::function_symbols::SortArrow)
1192 if (term.size() != 2)
1196#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1197 if (!check_list_argument(term[0], check_rule_SortExpr<atermpp::aterm>, 1))
1199 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
1202 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1204 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
1214template <atermpp::IsATerm Term>
1217#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1220 if (!term.type_is_appl())
1224 if (term.function() != core::detail::function_symbols::UntypedSortUnknown)
1230 if (term.size() != 0)
1240template <atermpp::IsATerm Term>
1243#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1246 if (!term.type_is_appl())
1250 if (term.function() != core::detail::function_symbols::UntypedSortsPossible)
1256 if (term.size() != 1)
1260#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1261 if (!check_list_argument(term[0], check_rule_SortExpr<atermpp::aterm>, 1))
1263 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
1273template <atermpp::IsATerm Term>
1276#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1279 if (!term.type_is_appl())
1283 if (term.function() != core::detail::function_symbols::UntypedSortVariable)
1289 if (term.size() != 1)
1293#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1294 if (!check_term_argument(term[0], check_rule_Number<atermpp::aterm>))
1296 mCRL2log(log::log_level_t::debug) <<
"check_rule_Number" << std::endl;
1306template <atermpp::IsATerm Term>
1309#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1312 if (!term.type_is_appl())
1316 if (term.function() != core::detail::function_symbols::SortId)
1322 if (term.size() != 1)
1326#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1327 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1329 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
1339template <atermpp::IsATerm Term>
1342#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1345 if (!term.type_is_appl())
1349 if (term.function() != core::detail::function_symbols::SortList)
1355 if (term.size() != 0)
1365template <atermpp::IsATerm Term>
1368#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1371 if (!term.type_is_appl())
1375 if (term.function() != core::detail::function_symbols::SortSet)
1381 if (term.size() != 0)
1391template <atermpp::IsATerm Term>
1394#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1397 if (!term.type_is_appl())
1401 if (term.function() != core::detail::function_symbols::SortBag)
1407 if (term.size() != 0)
1417template <atermpp::IsATerm Term>
1420#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1423 if (!term.type_is_appl())
1427 if (term.function() != core::detail::function_symbols::SortFSet)
1433 if (term.size() != 0)
1443template <atermpp::IsATerm Term>
1446#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1449 if (!term.type_is_appl())
1453 if (term.function() != core::detail::function_symbols::SortFBag)
1459 if (term.size() != 0)
1469template <atermpp::IsATerm Term>
1472#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1475 if (!term.type_is_appl())
1479 if (term.function() != core::detail::function_symbols::StructCons)
1485 if (term.size() != 3)
1489#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1490 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1492 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
1495 if (!check_list_argument(term[1], check_rule_StructProj<atermpp::aterm>, 0))
1497 mCRL2log(log::log_level_t::debug) <<
"check_rule_StructProj" << std::endl;
1500 if (!check_term_argument(term[2], check_rule_StringOrEmpty<atermpp::aterm>))
1502 mCRL2log(log::log_level_t::debug) <<
"check_rule_StringOrEmpty" << std::endl;
1512template <atermpp::IsATerm Term>
1515#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1518 if (!term.type_is_appl())
1522 if (term.function() != core::detail::function_symbols::StructProj)
1528 if (term.size() != 2)
1532#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1533 if (!check_term_argument(term[0], check_rule_StringOrEmpty<atermpp::aterm>))
1535 mCRL2log(log::log_level_t::debug) <<
"check_rule_StringOrEmpty" << std::endl;
1538 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1540 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
1550template <atermpp::IsATerm Term>
1553#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1556 if (!term.type_is_appl())
1560 if (term.function() != core::detail::function_symbols::Binder)
1566 if (term.size() != 3)
1570#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1571 if (!check_term_argument(term[0], check_rule_BindingOperator<atermpp::aterm>))
1573 mCRL2log(log::log_level_t::debug) <<
"check_rule_BindingOperator" << std::endl;
1576 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 1))
1578 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
1581 if (!check_term_argument(term[2], check_rule_DataExpr<atermpp::aterm>))
1583 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
1593template <atermpp::IsATerm Term>
1596#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1599 if (!term.type_is_appl())
1603 if (term.function() != core::detail::function_symbols::Whr)
1609 if (term.size() != 2)
1613#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1614 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
1616 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
1619 if (!check_list_argument(term[1], check_rule_WhrDecl<atermpp::aterm>, 1))
1621 mCRL2log(log::log_level_t::debug) <<
"check_rule_WhrDecl" << std::endl;
1631template <atermpp::IsATerm Term>
1634#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1637 if (!term.type_is_appl())
1641 if (term.function() != core::detail::function_symbols::UntypedIdentifier)
1647 if (term.size() != 1)
1651#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1652 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1654 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
1664template <atermpp::IsATerm Term>
1667#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1670 if (!term.type_is_appl())
1674 if (term.function() != core::detail::function_symbols::DataVarId)
1680 if (term.size() != 2)
1684#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1685 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1687 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
1690 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1692 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
1702template <atermpp::IsATerm Term>
1705#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1708 if (!term.type_is_appl())
1712 if (term.function() != core::detail::function_symbols::OpId)
1718 if (term.size() != 3)
1722#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1723 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1725 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
1728 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1730 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
1733 if (!check_term_argument(term[2], check_rule_Number<atermpp::aterm>))
1735 mCRL2log(log::log_level_t::debug) <<
"check_rule_Number" << std::endl;
1745template <atermpp::IsATerm Term>
1748#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1751 if (!term.type_is_appl())
1755 if (term.function() != core::detail::function_symbols::UntypedDataParameter)
1761 if (term.size() != 2)
1765#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1766 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1768 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
1771 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
1773 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
1783template <atermpp::IsATerm Term>
1786#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1789 if (!term.type_is_appl())
1793 if (term.function() != core::detail::function_symbols::Forall)
1799 if (term.size() != 0)
1809template <atermpp::IsATerm Term>
1812#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1815 if (!term.type_is_appl())
1819 if (term.function() != core::detail::function_symbols::Exists)
1825 if (term.size() != 0)
1835template <atermpp::IsATerm Term>
1838#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1841 if (!term.type_is_appl())
1845 if (term.function() != core::detail::function_symbols::SetComp)
1851 if (term.size() != 0)
1861template <atermpp::IsATerm Term>
1864#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1867 if (!term.type_is_appl())
1871 if (term.function() != core::detail::function_symbols::BagComp)
1877 if (term.size() != 0)
1887template <atermpp::IsATerm Term>
1890#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1893 if (!term.type_is_appl())
1897 if (term.function() != core::detail::function_symbols::Lambda)
1903 if (term.size() != 0)
1913template <atermpp::IsATerm Term>
1916#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1919 if (!term.type_is_appl())
1923 if (term.function() != core::detail::function_symbols::UntypedSetBagComp)
1929 if (term.size() != 0)
1939template <atermpp::IsATerm Term>
1942#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1945 if (!term.type_is_appl())
1949 if (term.function() != core::detail::function_symbols::DataVarIdInit)
1955 if (term.size() != 2)
1959#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1960 if (!check_term_argument(term[0], check_rule_DataVarId<atermpp::aterm>))
1962 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
1965 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
1967 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
1977template <atermpp::IsATerm Term>
1980#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1983 if (!term.type_is_appl())
1987 if (term.function() != core::detail::function_symbols::UntypedIdentifierAssignment)
1993 if (term.size() != 2)
1997#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1998 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
2000 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
2003 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2005 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2015template <atermpp::IsATerm Term>
2018#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2021 if (!term.type_is_appl())
2025 if (term.function() != core::detail::function_symbols::DataSpec)
2031 if (term.size() != 4)
2035#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2036 if (!check_term_argument(term[0], check_rule_SortSpec<atermpp::aterm>))
2038 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortSpec" << std::endl;
2041 if (!check_term_argument(term[1], check_rule_ConsSpec<atermpp::aterm>))
2043 mCRL2log(log::log_level_t::debug) <<
"check_rule_ConsSpec" << std::endl;
2046 if (!check_term_argument(term[2], check_rule_MapSpec<atermpp::aterm>))
2048 mCRL2log(log::log_level_t::debug) <<
"check_rule_MapSpec" << std::endl;
2051 if (!check_term_argument(term[3], check_rule_DataEqnSpec<atermpp::aterm>))
2053 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataEqnSpec" << std::endl;
2063template <atermpp::IsATerm Term>
2066#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2069 if (!term.type_is_appl())
2073 if (term.function() != core::detail::function_symbols::SortSpec)
2079 if (term.size() != 1)
2083#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2084 if (!check_list_argument(term[0], check_rule_SortDecl<atermpp::aterm>, 0))
2086 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortDecl" << std::endl;
2096template <atermpp::IsATerm Term>
2099#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2102 if (!term.type_is_appl())
2106 if (term.function() != core::detail::function_symbols::ConsSpec)
2112 if (term.size() != 1)
2116#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2117 if (!check_list_argument(term[0], check_rule_OpId<atermpp::aterm>, 0))
2119 mCRL2log(log::log_level_t::debug) <<
"check_rule_OpId" << std::endl;
2129template <atermpp::IsATerm Term>
2132#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2135 if (!term.type_is_appl())
2139 if (term.function() != core::detail::function_symbols::MapSpec)
2145 if (term.size() != 1)
2149#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2150 if (!check_list_argument(term[0], check_rule_OpId<atermpp::aterm>, 0))
2152 mCRL2log(log::log_level_t::debug) <<
"check_rule_OpId" << std::endl;
2162template <atermpp::IsATerm Term>
2165#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2168 if (!term.type_is_appl())
2172 if (term.function() != core::detail::function_symbols::DataEqnSpec)
2178 if (term.size() != 1)
2182#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2183 if (!check_list_argument(term[0], check_rule_DataEqn<atermpp::aterm>, 0))
2185 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataEqn" << std::endl;
2195template <atermpp::IsATerm Term>
2198#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2201 if (!term.type_is_appl())
2205 if (term.function() != core::detail::function_symbols::SortRef)
2211 if (term.size() != 2)
2215#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2216 if (!check_term_argument(term[0], check_rule_SortId<atermpp::aterm>))
2218 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortId" << std::endl;
2221 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
2223 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
2233template <atermpp::IsATerm Term>
2236#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2239 if (!term.type_is_appl())
2243 if (term.function() != core::detail::function_symbols::DataEqn)
2249 if (term.size() != 4)
2253#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2254 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
2256 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
2259 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2261 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2264 if (!check_term_argument(term[2], check_rule_DataExpr<atermpp::aterm>))
2266 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2269 if (!check_term_argument(term[3], check_rule_DataExpr<atermpp::aterm>))
2271 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2281template <atermpp::IsATerm Term>
2284#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2287 if (!term.type_is_appl())
2291 if (term.function() != core::detail::function_symbols::MultAct)
2297 if (term.size() != 1)
2301#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2302 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
2304 mCRL2log(log::log_level_t::debug) <<
"check_rule_Action" << std::endl;
2314template <atermpp::IsATerm Term>
2317#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2320 if (!term.type_is_appl())
2324 if (term.function() != core::detail::function_symbols::TimedMultAct)
2330 if (term.size() != 2)
2334#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2335 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
2337 mCRL2log(log::log_level_t::debug) <<
"check_rule_Action" << std::endl;
2340 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2342 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2352template <atermpp::IsATerm Term>
2355#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2358 if (!term.type_is_appl())
2362 if (term.function() != core::detail::function_symbols::UntypedMultiAction)
2368 if (term.size() != 1)
2372#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2373 if (!check_list_argument(term[0], check_rule_UntypedDataParameter<atermpp::aterm>, 0))
2375 mCRL2log(log::log_level_t::debug) <<
"check_rule_UntypedDataParameter" << std::endl;
2385template <atermpp::IsATerm Term>
2388#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2391 if (!term.type_is_appl())
2395 if (term.function() != core::detail::function_symbols::Action)
2401 if (term.size() != 2)
2405#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2406 if (!check_term_argument(term[0], check_rule_ActId<atermpp::aterm>))
2408 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActId" << std::endl;
2411 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
2413 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2423template <atermpp::IsATerm Term>
2426#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2429 if (!term.type_is_appl())
2433 if (term.function() != core::detail::function_symbols::ActId)
2439 if (term.size() != 2)
2443#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2444 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
2446 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
2449 if (!check_list_argument(term[1], check_rule_SortExpr<atermpp::aterm>, 0))
2451 mCRL2log(log::log_level_t::debug) <<
"check_rule_SortExpr" << std::endl;
2461template <atermpp::IsATerm Term>
2464#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2467 if (!term.type_is_appl())
2471 if (term.function() != core::detail::function_symbols::Process)
2477 if (term.size() != 2)
2481#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2482 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
2484 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcVarId" << std::endl;
2487 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
2489 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2499template <atermpp::IsATerm Term>
2502#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2505 if (!term.type_is_appl())
2509 if (term.function() != core::detail::function_symbols::ProcessAssignment)
2515 if (term.size() != 2)
2519#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2520 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
2522 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcVarId" << std::endl;
2525 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
2527 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarIdInit" << std::endl;
2537template <atermpp::IsATerm Term>
2540#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2543 if (!term.type_is_appl())
2547 if (term.function() != core::detail::function_symbols::Delta)
2553 if (term.size() != 0)
2563template <atermpp::IsATerm Term>
2566#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2569 if (!term.type_is_appl())
2573 if (term.function() != core::detail::function_symbols::Tau)
2579 if (term.size() != 0)
2589template <atermpp::IsATerm Term>
2592#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2595 if (!term.type_is_appl())
2599 if (term.function() != core::detail::function_symbols::Sum)
2605 if (term.size() != 2)
2609#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2610 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
2612 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
2615 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2617 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2627template <atermpp::IsATerm Term>
2630#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2633 if (!term.type_is_appl())
2637 if (term.function() != core::detail::function_symbols::Block)
2643 if (term.size() != 2)
2647#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2648 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 0))
2650 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
2653 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2655 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2665template <atermpp::IsATerm Term>
2668#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2671 if (!term.type_is_appl())
2675 if (term.function() != core::detail::function_symbols::Hide)
2681 if (term.size() != 2)
2685#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2686 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 0))
2688 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
2691 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2693 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2703template <atermpp::IsATerm Term>
2706#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2709 if (!term.type_is_appl())
2713 if (term.function() != core::detail::function_symbols::Rename)
2719 if (term.size() != 2)
2723#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2724 if (!check_list_argument(term[0], check_rule_RenameExpr<atermpp::aterm>, 0))
2726 mCRL2log(log::log_level_t::debug) <<
"check_rule_RenameExpr" << std::endl;
2729 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2731 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2741template <atermpp::IsATerm Term>
2744#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2747 if (!term.type_is_appl())
2751 if (term.function() != core::detail::function_symbols::Comm)
2757 if (term.size() != 2)
2761#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2762 if (!check_list_argument(term[0], check_rule_CommExpr<atermpp::aterm>, 0))
2764 mCRL2log(log::log_level_t::debug) <<
"check_rule_CommExpr" << std::endl;
2767 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2769 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2779template <atermpp::IsATerm Term>
2782#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2785 if (!term.type_is_appl())
2789 if (term.function() != core::detail::function_symbols::Allow)
2795 if (term.size() != 2)
2799#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2800 if (!check_list_argument(term[0], check_rule_MultActName<atermpp::aterm>, 0))
2802 mCRL2log(log::log_level_t::debug) <<
"check_rule_MultActName" << std::endl;
2805 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2807 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2817template <atermpp::IsATerm Term>
2820#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2823 if (!term.type_is_appl())
2827 if (term.function() != core::detail::function_symbols::Sync)
2833 if (term.size() != 2)
2837#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2838 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2840 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2843 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2845 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2855template <atermpp::IsATerm Term>
2858#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2861 if (!term.type_is_appl())
2865 if (term.function() != core::detail::function_symbols::AtTime)
2871 if (term.size() != 2)
2875#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2876 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2878 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2881 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2883 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2893template <atermpp::IsATerm Term>
2896#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2899 if (!term.type_is_appl())
2903 if (term.function() != core::detail::function_symbols::Seq)
2909 if (term.size() != 2)
2913#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2914 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2916 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2919 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2921 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2931template <atermpp::IsATerm Term>
2934#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2937 if (!term.type_is_appl())
2941 if (term.function() != core::detail::function_symbols::IfThen)
2947 if (term.size() != 2)
2951#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2952 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
2954 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2957 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2959 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
2969template <atermpp::IsATerm Term>
2972#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2975 if (!term.type_is_appl())
2979 if (term.function() != core::detail::function_symbols::IfThenElse)
2985 if (term.size() != 3)
2989#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2990 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
2992 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
2995 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2997 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3000 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3002 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3012template <atermpp::IsATerm Term>
3015#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3018 if (!term.type_is_appl())
3022 if (term.function() != core::detail::function_symbols::BInit)
3028 if (term.size() != 2)
3032#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3033 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3035 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3038 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3040 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3050template <atermpp::IsATerm Term>
3053#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3056 if (!term.type_is_appl())
3060 if (term.function() != core::detail::function_symbols::Merge)
3066 if (term.size() != 2)
3070#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3071 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3073 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3076 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3078 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3088template <atermpp::IsATerm Term>
3091#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3094 if (!term.type_is_appl())
3098 if (term.function() != core::detail::function_symbols::LMerge)
3104 if (term.size() != 2)
3108#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3109 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3111 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3114 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3116 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3126template <atermpp::IsATerm Term>
3129#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3132 if (!term.type_is_appl())
3136 if (term.function() != core::detail::function_symbols::Choice)
3142 if (term.size() != 2)
3146#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3147 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3149 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3152 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3154 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3164template <atermpp::IsATerm Term>
3167#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3170 if (!term.type_is_appl())
3174 if (term.function() != core::detail::function_symbols::StochasticOperator)
3180 if (term.size() != 3)
3184#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3185 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
3187 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
3190 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3192 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
3195 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3197 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3207template <atermpp::IsATerm Term>
3210#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3213 if (!term.type_is_appl())
3217 if (term.function() != core::detail::function_symbols::UntypedProcessAssignment)
3223 if (term.size() != 2)
3227#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3228 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3230 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
3233 if (!check_list_argument(term[1], check_rule_UntypedIdentifierAssignment<atermpp::aterm>, 0))
3235 mCRL2log(log::log_level_t::debug) <<
"check_rule_UntypedIdentifierAssignment" << std::endl;
3245template <atermpp::IsATerm Term>
3248#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3251 if (!term.type_is_appl())
3255 if (term.function() != core::detail::function_symbols::ProcVarId)
3261 if (term.size() != 2)
3265#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3266 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3268 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
3271 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
3273 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
3283template <atermpp::IsATerm Term>
3286#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3289 if (!term.type_is_appl())
3293 if (term.function() != core::detail::function_symbols::MultActName)
3299 if (term.size() != 1)
3303#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3304 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 1))
3306 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
3316template <atermpp::IsATerm Term>
3319#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3322 if (!term.type_is_appl())
3326 if (term.function() != core::detail::function_symbols::RenameExpr)
3332 if (term.size() != 2)
3336#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3337 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3339 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
3342 if (!check_term_argument(term[1], check_rule_String<atermpp::aterm>))
3344 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
3354template <atermpp::IsATerm Term>
3357#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3360 if (!term.type_is_appl())
3364 if (term.function() != core::detail::function_symbols::CommExpr)
3370 if (term.size() != 2)
3374#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3375 if (!check_term_argument(term[0], check_rule_MultActName<atermpp::aterm>))
3377 mCRL2log(log::log_level_t::debug) <<
"check_rule_MultActName" << std::endl;
3380 if (!check_term_argument(term[1], check_rule_String<atermpp::aterm>))
3382 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
3392template <atermpp::IsATerm Term>
3395#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3398 if (!term.type_is_appl())
3402 if (term.function() != core::detail::function_symbols::ProcSpec)
3408 if (term.size() != 5)
3412#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3413 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
3415 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataSpec" << std::endl;
3418 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
3420 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActSpec" << std::endl;
3423 if (!check_term_argument(term[2], check_rule_GlobVarSpec<atermpp::aterm>))
3425 mCRL2log(log::log_level_t::debug) <<
"check_rule_GlobVarSpec" << std::endl;
3428 if (!check_term_argument(term[3], check_rule_ProcEqnSpec<atermpp::aterm>))
3430 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcEqnSpec" << std::endl;
3433 if (!check_term_argument(term[4], check_rule_ProcInit<atermpp::aterm>))
3435 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcInit" << std::endl;
3445template <atermpp::IsATerm Term>
3448#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3451 if (!term.type_is_appl())
3455 if (term.function() != core::detail::function_symbols::ActSpec)
3461 if (term.size() != 1)
3465#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3466 if (!check_list_argument(term[0], check_rule_ActId<atermpp::aterm>, 0))
3468 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActId" << std::endl;
3478template <atermpp::IsATerm Term>
3481#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3484 if (!term.type_is_appl())
3488 if (term.function() != core::detail::function_symbols::GlobVarSpec)
3494 if (term.size() != 1)
3498#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3499 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3501 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
3511template <atermpp::IsATerm Term>
3514#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3517 if (!term.type_is_appl())
3521 if (term.function() != core::detail::function_symbols::ProcEqnSpec)
3527 if (term.size() != 1)
3531#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3532 if (!check_list_argument(term[0], check_rule_ProcEqn<atermpp::aterm>, 0))
3534 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcEqn" << std::endl;
3544template <atermpp::IsATerm Term>
3547#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3550 if (!term.type_is_appl())
3554 if (term.function() != core::detail::function_symbols::ProcEqn)
3560 if (term.size() != 3)
3564#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3565 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
3567 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcVarId" << std::endl;
3570 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
3572 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
3575 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3577 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3587template <atermpp::IsATerm Term>
3590#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3593 if (!term.type_is_appl())
3597 if (term.function() != core::detail::function_symbols::ProcessInit)
3603 if (term.size() != 1)
3607#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3608 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3610 mCRL2log(log::log_level_t::debug) <<
"check_rule_ProcExpr" << std::endl;
3620template <atermpp::IsATerm Term>
3623#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3626 if (!term.type_is_appl())
3630 if (term.function() != core::detail::function_symbols::Distribution)
3636 if (term.size() != 2)
3640#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3641 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3643 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
3646 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3648 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
3658template <atermpp::IsATerm Term>
3661#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3664 if (!term.type_is_appl())
3668 if (term.function() != core::detail::function_symbols::LinProcSpec)
3674 if (term.size() != 5)
3678#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3679 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
3681 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataSpec" << std::endl;
3684 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
3686 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActSpec" << std::endl;
3689 if (!check_term_argument(term[2], check_rule_GlobVarSpec<atermpp::aterm>))
3691 mCRL2log(log::log_level_t::debug) <<
"check_rule_GlobVarSpec" << std::endl;
3694 if (!check_term_argument(term[3], check_rule_LinearProcess<atermpp::aterm>))
3696 mCRL2log(log::log_level_t::debug) <<
"check_rule_LinearProcess" << std::endl;
3699 if (!check_term_argument(term[4], check_rule_LinearProcessInit<atermpp::aterm>))
3701 mCRL2log(log::log_level_t::debug) <<
"check_rule_LinearProcessInit" << std::endl;
3711template <atermpp::IsATerm Term>
3714#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3717 if (!term.type_is_appl())
3721 if (term.function() != core::detail::function_symbols::LinearProcess)
3727 if (term.size() != 2)
3731#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3732 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3734 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
3737 if (!check_list_argument(term[1], check_rule_LinearProcessSummand<atermpp::aterm>, 0))
3739 mCRL2log(log::log_level_t::debug) <<
"check_rule_LinearProcessSummand" << std::endl;
3749template <atermpp::IsATerm Term>
3752#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3755 if (!term.type_is_appl())
3759 if (term.function() != core::detail::function_symbols::LinearProcessSummand)
3765 if (term.size() != 6)
3769#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3770 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3772 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
3775 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3777 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
3780 if (!check_term_argument(term[2], check_rule_MultActOrDelta<atermpp::aterm>))
3782 mCRL2log(log::log_level_t::debug) <<
"check_rule_MultActOrDelta" << std::endl;
3785 if (!check_term_argument(term[3], check_rule_DataExpr<atermpp::aterm>))
3787 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
3790 if (!check_list_argument(term[4], check_rule_DataVarIdInit<atermpp::aterm>, 0))
3792 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarIdInit" << std::endl;
3795 if (!check_term_argument(term[5], check_rule_Distribution<atermpp::aterm>))
3797 mCRL2log(log::log_level_t::debug) <<
"check_rule_Distribution" << std::endl;
3807template <atermpp::IsATerm Term>
3810#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3813 if (!term.type_is_appl())
3817 if (term.function() != core::detail::function_symbols::LinearProcessInit)
3823 if (term.size() != 2)
3827#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3828 if (!check_list_argument(term[0], check_rule_DataExpr<atermpp::aterm>, 0))
3830 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
3833 if (!check_term_argument(term[1], check_rule_Distribution<atermpp::aterm>))
3835 mCRL2log(log::log_level_t::debug) <<
"check_rule_Distribution" << std::endl;
3845template <atermpp::IsATerm Term>
3848#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3851 if (!term.type_is_appl())
3855 if (term.function() != core::detail::function_symbols::StateTrue)
3861 if (term.size() != 0)
3871template <atermpp::IsATerm Term>
3874#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3877 if (!term.type_is_appl())
3881 if (term.function() != core::detail::function_symbols::StateFalse)
3887 if (term.size() != 0)
3897template <atermpp::IsATerm Term>
3900#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3903 if (!term.type_is_appl())
3907 if (term.function() != core::detail::function_symbols::StateNot)
3913 if (term.size() != 1)
3917#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3918 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
3920 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
3930template <atermpp::IsATerm Term>
3933#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3936 if (!term.type_is_appl())
3940 if (term.function() != core::detail::function_symbols::StateMinus)
3946 if (term.size() != 1)
3950#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3951 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
3953 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
3963template <atermpp::IsATerm Term>
3966#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3969 if (!term.type_is_appl())
3973 if (term.function() != core::detail::function_symbols::StateAnd)
3979 if (term.size() != 2)
3983#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3984 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
3986 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
3989 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
3991 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4001template <atermpp::IsATerm Term>
4004#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4007 if (!term.type_is_appl())
4011 if (term.function() != core::detail::function_symbols::StateOr)
4017 if (term.size() != 2)
4021#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4022 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4024 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4027 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4029 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4039template <atermpp::IsATerm Term>
4042#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4045 if (!term.type_is_appl())
4049 if (term.function() != core::detail::function_symbols::StateImp)
4055 if (term.size() != 2)
4059#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4060 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4062 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4065 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4067 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4077template <atermpp::IsATerm Term>
4080#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4083 if (!term.type_is_appl())
4087 if (term.function() != core::detail::function_symbols::StatePlus)
4093 if (term.size() != 2)
4097#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4098 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4100 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4103 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4105 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4115template <atermpp::IsATerm Term>
4118#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4121 if (!term.type_is_appl())
4125 if (term.function() != core::detail::function_symbols::StateConstantMultiply)
4131 if (term.size() != 2)
4135#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4136 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4138 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
4141 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4143 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4153template <atermpp::IsATerm Term>
4156#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4159 if (!term.type_is_appl())
4163 if (term.function() != core::detail::function_symbols::StateConstantMultiplyAlt)
4169 if (term.size() != 2)
4173#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4174 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4176 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4179 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
4181 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
4191template <atermpp::IsATerm Term>
4194#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4197 if (!term.type_is_appl())
4201 if (term.function() != core::detail::function_symbols::StateForall)
4207 if (term.size() != 2)
4211#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4212 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4214 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
4217 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4219 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4229template <atermpp::IsATerm Term>
4232#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4235 if (!term.type_is_appl())
4239 if (term.function() != core::detail::function_symbols::StateExists)
4245 if (term.size() != 2)
4249#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4250 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4252 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
4255 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4257 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4267template <atermpp::IsATerm Term>
4270#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4273 if (!term.type_is_appl())
4277 if (term.function() != core::detail::function_symbols::StateInfimum)
4283 if (term.size() != 2)
4287#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4288 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4290 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
4293 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4295 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4305template <atermpp::IsATerm Term>
4308#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4311 if (!term.type_is_appl())
4315 if (term.function() != core::detail::function_symbols::StateSupremum)
4321 if (term.size() != 2)
4325#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4326 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4328 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
4331 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4333 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4343template <atermpp::IsATerm Term>
4346#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4349 if (!term.type_is_appl())
4353 if (term.function() != core::detail::function_symbols::StateSum)
4359 if (term.size() != 2)
4363#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4364 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4366 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
4369 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4371 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4381template <atermpp::IsATerm Term>
4384#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4387 if (!term.type_is_appl())
4391 if (term.function() != core::detail::function_symbols::StateMust)
4397 if (term.size() != 2)
4401#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4402 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4404 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4407 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4409 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4419template <atermpp::IsATerm Term>
4422#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4425 if (!term.type_is_appl())
4429 if (term.function() != core::detail::function_symbols::StateMay)
4435 if (term.size() != 2)
4439#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4440 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4442 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4445 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4447 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4457template <atermpp::IsATerm Term>
4460#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4463 if (!term.type_is_appl())
4467 if (term.function() != core::detail::function_symbols::StateYaled)
4473 if (term.size() != 0)
4483template <atermpp::IsATerm Term>
4486#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4489 if (!term.type_is_appl())
4493 if (term.function() != core::detail::function_symbols::StateYaledTimed)
4499 if (term.size() != 1)
4503#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4504 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4506 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
4516template <atermpp::IsATerm Term>
4519#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4522 if (!term.type_is_appl())
4526 if (term.function() != core::detail::function_symbols::StateDelay)
4532 if (term.size() != 0)
4542template <atermpp::IsATerm Term>
4545#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4548 if (!term.type_is_appl())
4552 if (term.function() != core::detail::function_symbols::StateDelayTimed)
4558 if (term.size() != 1)
4562#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4563 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4565 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
4575template <atermpp::IsATerm Term>
4578#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4581 if (!term.type_is_appl())
4585 if (term.function() != core::detail::function_symbols::StateVar)
4591 if (term.size() != 2)
4595#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4596 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4598 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
4601 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
4603 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
4613template <atermpp::IsATerm Term>
4616#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4619 if (!term.type_is_appl())
4623 if (term.function() != core::detail::function_symbols::StateNu)
4629 if (term.size() != 3)
4633#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4634 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4636 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
4639 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
4641 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarIdInit" << std::endl;
4644 if (!check_term_argument(term[2], check_rule_StateFrm<atermpp::aterm>))
4646 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4656template <atermpp::IsATerm Term>
4659#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4662 if (!term.type_is_appl())
4666 if (term.function() != core::detail::function_symbols::StateMu)
4672 if (term.size() != 3)
4676#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4677 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4679 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
4682 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
4684 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarIdInit" << std::endl;
4687 if (!check_term_argument(term[2], check_rule_StateFrm<atermpp::aterm>))
4689 mCRL2log(log::log_level_t::debug) <<
"check_rule_StateFrm" << std::endl;
4699template <atermpp::IsATerm Term>
4702#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4705 if (!term.type_is_appl())
4709 if (term.function() != core::detail::function_symbols::RegNil)
4715 if (term.size() != 0)
4725template <atermpp::IsATerm Term>
4728#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4731 if (!term.type_is_appl())
4735 if (term.function() != core::detail::function_symbols::RegSeq)
4741 if (term.size() != 2)
4745#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4746 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4748 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4751 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4753 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4763template <atermpp::IsATerm Term>
4766#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4769 if (!term.type_is_appl())
4773 if (term.function() != core::detail::function_symbols::RegAlt)
4779 if (term.size() != 2)
4783#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4784 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4786 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4789 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4791 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4801template <atermpp::IsATerm Term>
4804#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4807 if (!term.type_is_appl())
4811 if (term.function() != core::detail::function_symbols::RegTrans)
4817 if (term.size() != 1)
4821#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4822 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4824 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4834template <atermpp::IsATerm Term>
4837#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4840 if (!term.type_is_appl())
4844 if (term.function() != core::detail::function_symbols::RegTransOrNil)
4850 if (term.size() != 1)
4854#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4855 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4857 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4867template <atermpp::IsATerm Term>
4870#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4873 if (!term.type_is_appl())
4877 if (term.function() != core::detail::function_symbols::UntypedRegFrm)
4883 if (term.size() != 3)
4887#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4888 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4890 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
4893 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4895 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4898 if (!check_term_argument(term[2], check_rule_RegFrm<atermpp::aterm>))
4900 mCRL2log(log::log_level_t::debug) <<
"check_rule_RegFrm" << std::endl;
4910template <atermpp::IsATerm Term>
4913#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4916 if (!term.type_is_appl())
4920 if (term.function() != core::detail::function_symbols::ActTrue)
4926 if (term.size() != 0)
4936template <atermpp::IsATerm Term>
4939#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4942 if (!term.type_is_appl())
4946 if (term.function() != core::detail::function_symbols::ActFalse)
4952 if (term.size() != 0)
4962template <atermpp::IsATerm Term>
4965#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4968 if (!term.type_is_appl())
4972 if (term.function() != core::detail::function_symbols::ActNot)
4978 if (term.size() != 1)
4982#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4983 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
4985 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
4995template <atermpp::IsATerm Term>
4998#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5001 if (!term.type_is_appl())
5005 if (term.function() != core::detail::function_symbols::ActAnd)
5011 if (term.size() != 2)
5015#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5016 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5018 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5021 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5023 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5033template <atermpp::IsATerm Term>
5036#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5039 if (!term.type_is_appl())
5043 if (term.function() != core::detail::function_symbols::ActOr)
5049 if (term.size() != 2)
5053#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5054 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5056 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5059 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5061 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5071template <atermpp::IsATerm Term>
5074#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5077 if (!term.type_is_appl())
5081 if (term.function() != core::detail::function_symbols::ActImp)
5087 if (term.size() != 2)
5091#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5092 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5094 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5097 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5099 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5109template <atermpp::IsATerm Term>
5112#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5115 if (!term.type_is_appl())
5119 if (term.function() != core::detail::function_symbols::ActForall)
5125 if (term.size() != 2)
5129#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5130 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5132 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
5135 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5137 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5147template <atermpp::IsATerm Term>
5150#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5153 if (!term.type_is_appl())
5157 if (term.function() != core::detail::function_symbols::ActExists)
5163 if (term.size() != 2)
5167#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5168 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5170 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
5173 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5175 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5185template <atermpp::IsATerm Term>
5188#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5191 if (!term.type_is_appl())
5195 if (term.function() != core::detail::function_symbols::ActAt)
5201 if (term.size() != 2)
5205#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5206 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5208 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActFrm" << std::endl;
5211 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
5213 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
5223template <atermpp::IsATerm Term>
5226#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5229 if (!term.type_is_appl())
5233 if (term.function() != core::detail::function_symbols::ActMultAct)
5239 if (term.size() != 1)
5243#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5244 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
5246 mCRL2log(log::log_level_t::debug) <<
"check_rule_Action" << std::endl;
5256template <atermpp::IsATerm Term>
5259#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5262 if (!term.type_is_appl())
5266 if (term.function() != core::detail::function_symbols::ActionRenameRules)
5272 if (term.size() != 1)
5276#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5277 if (!check_list_argument(term[0], check_rule_ActionRenameRule<atermpp::aterm>, 0))
5279 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActionRenameRule" << std::endl;
5289template <atermpp::IsATerm Term>
5292#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5295 if (!term.type_is_appl())
5299 if (term.function() != core::detail::function_symbols::ActionRenameRule)
5305 if (term.size() != 4)
5309#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5310 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
5312 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
5315 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
5317 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
5320 if (!check_term_argument(term[2], check_rule_ParamIdOrAction<atermpp::aterm>))
5322 mCRL2log(log::log_level_t::debug) <<
"check_rule_ParamIdOrAction" << std::endl;
5325 if (!check_term_argument(term[3], check_rule_ActionRenameRuleRHS<atermpp::aterm>))
5327 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActionRenameRuleRHS" << std::endl;
5337template <atermpp::IsATerm Term>
5340#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5343 if (!term.type_is_appl())
5347 if (term.function() != core::detail::function_symbols::ActionRenameSpec)
5353 if (term.size() != 3)
5357#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5358 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
5360 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataSpec" << std::endl;
5363 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
5365 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActSpec" << std::endl;
5368 if (!check_term_argument(term[2], check_rule_ActionRenameRules<atermpp::aterm>))
5370 mCRL2log(log::log_level_t::debug) <<
"check_rule_ActionRenameRules" << std::endl;
5380template <atermpp::IsATerm Term>
5383#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5386 if (!term.type_is_appl())
5390 if (term.function() != core::detail::function_symbols::PBES)
5396 if (term.size() != 4)
5400#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5401 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
5403 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataSpec" << std::endl;
5406 if (!check_term_argument(term[1], check_rule_GlobVarSpec<atermpp::aterm>))
5408 mCRL2log(log::log_level_t::debug) <<
"check_rule_GlobVarSpec" << std::endl;
5411 if (!check_term_argument(term[2], check_rule_PBEqnSpec<atermpp::aterm>))
5413 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBEqnSpec" << std::endl;
5416 if (!check_term_argument(term[3], check_rule_PBInit<atermpp::aterm>))
5418 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBInit" << std::endl;
5428template <atermpp::IsATerm Term>
5431#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5434 if (!term.type_is_appl())
5438 if (term.function() != core::detail::function_symbols::PBEqnSpec)
5444 if (term.size() != 1)
5448#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5449 if (!check_list_argument(term[0], check_rule_PBEqn<atermpp::aterm>, 0))
5451 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBEqn" << std::endl;
5461template <atermpp::IsATerm Term>
5464#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5467 if (!term.type_is_appl())
5471 if (term.function() != core::detail::function_symbols::PBInit)
5477 if (term.size() != 1)
5481#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5482 if (!check_term_argument(term[0], check_rule_PropVarInst<atermpp::aterm>))
5484 mCRL2log(log::log_level_t::debug) <<
"check_rule_PropVarInst" << std::endl;
5494template <atermpp::IsATerm Term>
5497#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5500 if (!term.type_is_appl())
5504 if (term.function() != core::detail::function_symbols::PBEqn)
5510 if (term.size() != 3)
5514#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5515 if (!check_term_argument(term[0], check_rule_FixPoint<atermpp::aterm>))
5517 mCRL2log(log::log_level_t::debug) <<
"check_rule_FixPoint" << std::endl;
5520 if (!check_term_argument(term[1], check_rule_PropVarDecl<atermpp::aterm>))
5522 mCRL2log(log::log_level_t::debug) <<
"check_rule_PropVarDecl" << std::endl;
5525 if (!check_term_argument(term[2], check_rule_PBExpr<atermpp::aterm>))
5527 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5537template <atermpp::IsATerm Term>
5540#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5543 if (!term.type_is_appl())
5547 if (term.function() != core::detail::function_symbols::Mu)
5553 if (term.size() != 0)
5563template <atermpp::IsATerm Term>
5566#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5569 if (!term.type_is_appl())
5573 if (term.function() != core::detail::function_symbols::Nu)
5579 if (term.size() != 0)
5589template <atermpp::IsATerm Term>
5592#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5595 if (!term.type_is_appl())
5599 if (term.function() != core::detail::function_symbols::PropVarDecl)
5605 if (term.size() != 2)
5609#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5610 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
5612 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
5615 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
5617 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
5627template <atermpp::IsATerm Term>
5630#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5633 if (!term.type_is_appl())
5637 if (term.function() != core::detail::function_symbols::PBESTrue)
5643 if (term.size() != 0)
5653template <atermpp::IsATerm Term>
5656#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5659 if (!term.type_is_appl())
5663 if (term.function() != core::detail::function_symbols::PBESFalse)
5669 if (term.size() != 0)
5679template <atermpp::IsATerm Term>
5682#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5685 if (!term.type_is_appl())
5689 if (term.function() != core::detail::function_symbols::PBESNot)
5695 if (term.size() != 1)
5699#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5700 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5702 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5712template <atermpp::IsATerm Term>
5715#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5718 if (!term.type_is_appl())
5722 if (term.function() != core::detail::function_symbols::PBESAnd)
5728 if (term.size() != 2)
5732#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5733 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5735 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5738 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5740 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5750template <atermpp::IsATerm Term>
5753#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5756 if (!term.type_is_appl())
5760 if (term.function() != core::detail::function_symbols::PBESOr)
5766 if (term.size() != 2)
5770#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5771 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5773 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5776 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5778 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5788template <atermpp::IsATerm Term>
5791#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5794 if (!term.type_is_appl())
5798 if (term.function() != core::detail::function_symbols::PBESImp)
5804 if (term.size() != 2)
5808#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5809 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5811 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5814 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5816 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5826template <atermpp::IsATerm Term>
5829#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5832 if (!term.type_is_appl())
5836 if (term.function() != core::detail::function_symbols::PBESForall)
5842 if (term.size() != 2)
5846#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5847 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5849 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
5852 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5854 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5864template <atermpp::IsATerm Term>
5867#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5870 if (!term.type_is_appl())
5874 if (term.function() != core::detail::function_symbols::PBESExists)
5880 if (term.size() != 2)
5884#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5885 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5887 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
5890 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5892 mCRL2log(log::log_level_t::debug) <<
"check_rule_PBExpr" << std::endl;
5902template <atermpp::IsATerm Term>
5905#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5908 if (!term.type_is_appl())
5912 if (term.function() != core::detail::function_symbols::PropVarInst)
5918 if (term.size() != 2)
5922#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5923 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
5925 mCRL2log(log::log_level_t::debug) <<
"check_rule_String" << std::endl;
5928 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
5930 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
5940template <atermpp::IsATerm Term>
5943#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5946 if (!term.type_is_appl())
5950 if (term.function() != core::detail::function_symbols::PRES)
5956 if (term.size() != 4)
5960#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5961 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
5963 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataSpec" << std::endl;
5966 if (!check_term_argument(term[1], check_rule_GlobVarSpec<atermpp::aterm>))
5968 mCRL2log(log::log_level_t::debug) <<
"check_rule_GlobVarSpec" << std::endl;
5971 if (!check_term_argument(term[2], check_rule_PREqnSpec<atermpp::aterm>))
5973 mCRL2log(log::log_level_t::debug) <<
"check_rule_PREqnSpec" << std::endl;
5976 if (!check_term_argument(term[3], check_rule_PRInit<atermpp::aterm>))
5978 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRInit" << std::endl;
5988template <atermpp::IsATerm Term>
5991#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5994 if (!term.type_is_appl())
5998 if (term.function() != core::detail::function_symbols::PREqnSpec)
6004 if (term.size() != 1)
6008#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6009 if (!check_list_argument(term[0], check_rule_PREqn<atermpp::aterm>, 0))
6011 mCRL2log(log::log_level_t::debug) <<
"check_rule_PREqn" << std::endl;
6021template <atermpp::IsATerm Term>
6024#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6027 if (!term.type_is_appl())
6031 if (term.function() != core::detail::function_symbols::PRInit)
6037 if (term.size() != 1)
6041#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6042 if (!check_term_argument(term[0], check_rule_PropVarInst<atermpp::aterm>))
6044 mCRL2log(log::log_level_t::debug) <<
"check_rule_PropVarInst" << std::endl;
6054template <atermpp::IsATerm Term>
6057#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6060 if (!term.type_is_appl())
6064 if (term.function() != core::detail::function_symbols::PREqn)
6070 if (term.size() != 3)
6074#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6075 if (!check_term_argument(term[0], check_rule_FixPoint<atermpp::aterm>))
6077 mCRL2log(log::log_level_t::debug) <<
"check_rule_FixPoint" << std::endl;
6080 if (!check_term_argument(term[1], check_rule_PropVarDecl<atermpp::aterm>))
6082 mCRL2log(log::log_level_t::debug) <<
"check_rule_PropVarDecl" << std::endl;
6085 if (!check_term_argument(term[2], check_rule_PRExpr<atermpp::aterm>))
6087 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6097template <atermpp::IsATerm Term>
6100#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6103 if (!term.type_is_appl())
6107 if (term.function() != core::detail::function_symbols::PRESTrue)
6113 if (term.size() != 0)
6123template <atermpp::IsATerm Term>
6126#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6129 if (!term.type_is_appl())
6133 if (term.function() != core::detail::function_symbols::PRESFalse)
6139 if (term.size() != 0)
6149template <atermpp::IsATerm Term>
6152#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6155 if (!term.type_is_appl())
6159 if (term.function() != core::detail::function_symbols::PRESMinus)
6165 if (term.size() != 1)
6169#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6170 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6172 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6182template <atermpp::IsATerm Term>
6185#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6188 if (!term.type_is_appl())
6192 if (term.function() != core::detail::function_symbols::PRESAnd)
6198 if (term.size() != 2)
6202#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6203 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6205 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6208 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6210 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6220template <atermpp::IsATerm Term>
6223#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6226 if (!term.type_is_appl())
6230 if (term.function() != core::detail::function_symbols::PRESOr)
6236 if (term.size() != 2)
6240#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6241 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6243 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6246 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6248 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6258template <atermpp::IsATerm Term>
6261#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6264 if (!term.type_is_appl())
6268 if (term.function() != core::detail::function_symbols::PRESImp)
6274 if (term.size() != 2)
6278#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6279 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6281 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6284 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6286 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6296template <atermpp::IsATerm Term>
6299#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6302 if (!term.type_is_appl())
6306 if (term.function() != core::detail::function_symbols::PRESPlus)
6312 if (term.size() != 2)
6316#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6317 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6319 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6322 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6324 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6334template <atermpp::IsATerm Term>
6337#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6340 if (!term.type_is_appl())
6344 if (term.function() != core::detail::function_symbols::PRESConstantMultiply)
6350 if (term.size() != 2)
6354#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6355 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
6357 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
6360 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6362 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6372template <atermpp::IsATerm Term>
6375#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6378 if (!term.type_is_appl())
6382 if (term.function() != core::detail::function_symbols::PRESConstantMultiplyAlt)
6388 if (term.size() != 2)
6392#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6393 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6395 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6398 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
6400 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataExpr" << std::endl;
6410template <atermpp::IsATerm Term>
6413#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6416 if (!term.type_is_appl())
6420 if (term.function() != core::detail::function_symbols::PRESInfimum)
6426 if (term.size() != 2)
6430#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6431 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
6433 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
6436 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6438 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6448template <atermpp::IsATerm Term>
6451#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6454 if (!term.type_is_appl())
6458 if (term.function() != core::detail::function_symbols::PRESSupremum)
6464 if (term.size() != 2)
6468#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6469 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
6471 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
6474 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6476 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6486template <atermpp::IsATerm Term>
6489#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6492 if (!term.type_is_appl())
6496 if (term.function() != core::detail::function_symbols::PRESSum)
6502 if (term.size() != 2)
6506#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6507 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
6509 mCRL2log(log::log_level_t::debug) <<
"check_rule_DataVarId" << std::endl;
6512 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6514 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6524template <atermpp::IsATerm Term>
6527#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6530 if (!term.type_is_appl())
6534 if (term.function() != core::detail::function_symbols::PRESEqInf)
6540 if (term.size() != 1)
6544#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6545 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6547 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6557template <atermpp::IsATerm Term>
6560#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6563 if (!term.type_is_appl())
6567 if (term.function() != core::detail::function_symbols::PRESEqNInf)
6573 if (term.size() != 1)
6577#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6578 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6580 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6590template <atermpp::IsATerm Term>
6593#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6596 if (!term.type_is_appl())
6600 if (term.function() != core::detail::function_symbols::PRESCondSm)
6606 if (term.size() != 3)
6610#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6611 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6613 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6616 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6618 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6621 if (!check_term_argument(term[2], check_rule_PRExpr<atermpp::aterm>))
6623 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6633template <atermpp::IsATerm Term>
6636#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6639 if (!term.type_is_appl())
6643 if (term.function() != core::detail::function_symbols::PRESCondEq)
6649 if (term.size() != 3)
6653#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6654 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6656 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6659 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6661 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
6664 if (!check_term_argument(term[2], check_rule_PRExpr<atermpp::aterm>))
6666 mCRL2log(log::log_level_t::debug) <<
"check_rule_PRExpr" << std::endl;
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A unordered_map class in which aterms can be stored.
apply_builder_arg1(const Arg1 &arg1)
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
void apply(T &result, const argument_type &x)
An abstraction expression.
const variable_list & variables() const
const data_expression & body() const
alias()
\brief Default constructor X3.
alias(const alias &) noexcept=default
Move semantics.
alias & operator=(const alias &) noexcept=default
alias(const basic_sort &name, const sort_expression &reference)
\brief Constructor Z12.
alias(alias &&) noexcept=default
alias(const atermpp::aterm &term)
alias & operator=(alias &&) noexcept=default
const basic_sort & name() const
const sort_expression & reference() const
\brief Assignment expression
\brief Assignment of a data expression to a variable
const data_expression & rhs() const
const variable & lhs() const
universal quantification.
basic_sort(const basic_sort &) noexcept=default
Move semantics.
basic_sort()
\brief Default constructor X3.
basic_sort & operator=(const basic_sort &) noexcept=default
const core::identifier_string & name() const
basic_sort(basic_sort &&) noexcept=default
basic_sort(const core::identifier_string &name)
\brief Constructor Z14.
basic_sort(const std::string &name)
\brief Constructor Z2.
basic_sort & operator=(basic_sort &&) noexcept=default
basic_sort(const atermpp::aterm &term)
container_sort(const container_type &container_name, const sort_expression &element_sort)
\brief Constructor Z14.
const container_type & container_name() const
const sort_expression & element_sort() const
container_sort(const atermpp::aterm &term)
const data_expression & lhs() const
const data_expression & condition() const
const data_expression & rhs() const
const variable_list & variables() const
sort_expression sort() const
Returns the sort of the data expression.
existential quantification.
universal quantification.
const sort_expression & codomain() const
const sort_expression_list & domain() const
const core::identifier_string & name() const
const sort_expression & sort() const
universal quantification.
sort_expression & operator=(const sort_expression &) noexcept=default
sort_expression(const sort_expression &) noexcept=default
Move semantics.
sort_expression & operator=(sort_expression &&) noexcept=default
const sort_expression & target_sort() const
Returns the target sort of this expression.
sort_expression(sort_expression &&) noexcept=default
sort_expression()
\brief Default constructor X3.
sort_expression(const atermpp::aterm &term)
\brief An argument of a constructor of a structured sort
const core::identifier_string & name() const
const sort_expression & sort() const
\brief A constructor for a structured sort
const core::identifier_string & name() const
const core::identifier_string & recogniser() const
const structured_sort_constructor_argument_list & arguments() const
const structured_sort_constructor_list & constructors() const
\brief An untyped parameter
const core::identifier_string & name() const
const data_expression_list & arguments() const
\brief Assignment of a data expression to a string
const core::identifier_string & lhs() const
const data_expression & rhs() const
\brief An untyped identifier
\brief Multiple possible sorts
const sort_expression_list & sorts() const
universal quantification.
\brief Untyped sort variable
\brief Unknown sort expression
untyped_sort()
\brief Default constructor X3.
const core::identifier_string & name() const
const sort_expression & sort() const
\brief A where expression
const data_expression & body() const
const assignment_expression_list & declarations() const
D_ParserTables parser_tables_mcrl2
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
const aterm_string & empty_string()
Returns the empty aterm_string.
bool check_term_PREqnSpec(const Term &t)
bool check_term_MapSpec(const Term &t)
bool check_term_PBESTrue(const Term &t)
bool check_term_Seq(const Term &t)
bool check_term_DataVarIdInit(const Term &t)
bool check_rule_DataVarIdInit(const Term &t)
bool check_term_Action(const Term &t)
bool check_term_PRESOr(const Term &t)
bool check_term_SortId(const Term &t)
bool check_term_Sum(const Term &t)
bool check_term_Whr(const Term &t)
bool check_term_ActAt(const Term &t)
bool check_rule_WhrDecl(const Term &t)
bool check_term_StateInfimum(const Term &t)
bool check_term_CommExpr(const Term &t)
bool check_rule_ActSpec(const Term &t)
bool check_term_UntypedSortUnknown(const Term &t)
bool check_term_ActFalse(const Term &t)
bool check_term_ActId(const Term &t)
bool check_term_RegTrans(const Term &t)
bool check_rule_Distribution(const Term &t)
bool check_term_LinearProcessSummand(const Term &t)
bool check_rule_Number(const Term &t)
bool check_term_StateFalse(const Term &t)
bool check_term_argument(const Term &t, CheckFunction f)
bool check_term_UntypedSortVariable(const Term &t)
bool check_rule_ActFrm(const Term &t)
bool check_term_MultAct(const Term &t)
bool check_term_Tau(const Term &t)
bool check_rule_ActId(const Term &t)
bool check_term_UntypedProcessAssignment(const Term &t)
bool check_term_StateDelayTimed(const Term &t)
bool check_term_Delta(const Term &t)
bool check_rule_PBEqn(const Term &t)
bool check_rule_Action(const Term &t)
bool check_term_PRESTrue(const Term &t)
bool check_rule_ActionRenameSpec(const Term &t)
bool check_rule_FixPoint(const Term &t)
bool check_list_argument(const Term &t, CheckFunction f, unsigned int minimum_size)
bool check_rule_DataEqn(const Term &t)
bool check_rule_LinProcSpec(const Term &t)
bool check_term_PRES(const Term &t)
bool check_rule_SortDecl(const Term &t)
bool check_rule_RenameExpr(const Term &t)
bool check_term_ActImp(const Term &t)
bool check_term_Allow(const Term &t)
bool check_term_Choice(const Term &t)
bool check_term_LinProcSpec(const Term &t)
bool check_rule_SortId(const Term &t)
bool check_term_PBESNot(const Term &t)
bool check_term_Sync(const Term &t)
bool check_rule_String(const Term &t)
bool check_term_ActMultAct(const Term &t)
bool check_term_PRESCondEq(const Term &t)
bool check_term_RegTransOrNil(const Term &t)
bool check_term_GlobVarSpec(const Term &t)
bool check_term_StateSupremum(const Term &t)
bool check_term_Mu(const Term &t)
bool check_rule_BindingOperator(const Term &t)
bool check_rule_CommExpr(const Term &t)
bool check_term_UntypedIdentifierAssignment(const Term &t)
bool check_term_RegNil(const Term &t)
bool check_term_DataEqn(const Term &t)
bool check_term_UntypedIdentifier(const Term &t)
bool check_term_StateMust(const Term &t)
bool check_rule_StructProj(const Term &t)
bool check_rule_ConsSpec(const Term &t)
bool check_term_ProcEqnSpec(const Term &t)
bool check_term_LMerge(const Term &t)
bool check_term_ConsSpec(const Term &t)
bool check_rule_SortConsType(const Term &t)
bool check_term_SortSet(const Term &t)
bool check_rule_SortSpec(const Term &t)
bool check_rule_PRES(const Term &t)
bool check_term_Binder(const Term &t)
bool check_term_SortArrow(const Term &t)
bool check_rule_DataExpr(const Term &t)
bool check_term_StateSum(const Term &t)
bool check_term_DataVarId(const Term &t)
bool check_term_UntypedDataParameter(const Term &t)
bool check_term_PRESConstantMultiply(const Term &t)
bool check_term_PBESForall(const Term &t)
bool check_rule_DataEqnSpec(const Term &t)
bool check_term_ActTrue(const Term &t)
bool check_rule_MultActOrDelta(const Term &t)
bool check_rule_LinearProcess(const Term &t)
bool check_term_ProcessInit(const Term &t)
bool check_term_BagComp(const Term &t)
bool check_rule_ProcVarId(const Term &t)
bool check_term_SortFBag(const Term &t)
bool check_rule_PRExpr(const Term &t)
bool check_term_StateYaled(const Term &t)
bool check_term_MultActName(const Term &t)
bool check_term_Nu(const Term &t)
bool check_term_PBESExists(const Term &t)
bool check_term_BInit(const Term &t)
bool check_term_ProcessAssignment(const Term &t)
bool check_term_Lambda(const Term &t)
bool check_term_StateMay(const Term &t)
bool check_term_PRESAnd(const Term &t)
bool check_term_StateVar(const Term &t)
bool check_term_SortRef(const Term &t)
bool check_term_PRESEqInf(const Term &t)
bool check_rule_StateFrm(const Term &t)
bool check_term_ProcSpec(const Term &t)
bool check_term_SortBag(const Term &t)
bool check_term_ProcEqn(const Term &t)
bool check_rule_MultActName(const Term &t)
bool check_term_StatePlus(const Term &t)
bool check_term_TimedMultAct(const Term &t)
bool check_term_PRESInfimum(const Term &t)
bool check_term_Rename(const Term &t)
bool check_rule_MapSpec(const Term &t)
bool check_rule_ProcEqnSpec(const Term &t)
bool check_rule_ProcEqn(const Term &t)
bool check_rule_PREqn(const Term &t)
bool check_term_StateYaledTimed(const Term &t)
bool check_term_StateImp(const Term &t)
bool check_term_StateConstantMultiply(const Term &t)
bool check_rule_DataVarId(const Term &t)
bool check_rule_UntypedIdentifierAssignment(const Term &t)
bool check_term_SortCons(const Term &t)
bool check_term_PRESSupremum(const Term &t)
bool check_term_PropVarInst(const Term &t)
bool check_term_UntypedRegFrm(const Term &t)
bool check_rule_PBES(const Term &t)
bool check_term_IfThen(const Term &t)
bool check_term_ActForall(const Term &t)
bool check_term_StateTrue(const Term &t)
bool check_term_SortSpec(const Term &t)
bool check_term_StateOr(const Term &t)
bool check_term_Forall(const Term &t)
bool check_term_UntypedSetBagComp(const Term &t)
bool check_term_LinearProcess(const Term &t)
bool check_term_PBInit(const Term &t)
bool check_rule_ProcExpr(const Term &t)
bool check_term_Comm(const Term &t)
bool check_term_StateAnd(const Term &t)
bool check_term_PBESOr(const Term &t)
bool check_term_StateMinus(const Term &t)
bool check_term_RenameExpr(const Term &t)
bool check_term_ActExists(const Term &t)
bool check_term_LinearProcessInit(const Term &t)
bool check_rule_SortExpr(const Term &t)
bool check_term_PREqn(const Term &t)
bool check_term_UntypedMultiAction(const Term &t)
bool check_term_PBES(const Term &t)
bool check_rule_GlobVarSpec(const Term &t)
bool check_rule_ActionRenameRuleRHS(const Term &t)
bool check_term_ActAnd(const Term &t)
bool check_rule_DataSpec(const Term &t)
bool check_term_AtTime(const Term &t)
bool check_term_ActSpec(const Term &t)
bool check_term_StateMu(const Term &t)
bool check_rule_LinearProcessSummand(const Term &t)
bool check_rule_StringOrEmpty(const Term &t)
bool check_term_StateNu(const Term &t)
bool check_term_PBEqn(const Term &t)
bool check_term_PRESSum(const Term &t)
bool check_term_ActionRenameSpec(const Term &t)
bool check_term_StateDelay(const Term &t)
bool check_rule_PBEqnSpec(const Term &t)
bool check_term_SortStruct(const Term &t)
bool check_rule_RegFrm(const Term &t)
bool check_rule_ActionRenameRules(const Term &t)
bool check_term_StochasticOperator(const Term &t)
bool check_rule_ProcSpec(const Term &t)
bool check_term_PBESImp(const Term &t)
bool gsIsDataAppl(const atermpp::aterm &Term)
bool check_rule_PropVarDecl(const Term &t)
bool check_term_StateForall(const Term &t)
bool check_term_PRInit(const Term &t)
bool check_term_DataEqnSpec(const Term &t)
bool check_term_StructCons(const Term &t)
bool check_rule_ParamIdOrAction(const Term &t)
bool check_term_ProcVarId(const Term &t)
bool check_term_PRESConstantMultiplyAlt(const Term &t)
bool check_term_DataSpec(const Term &t)
bool check_term_Process(const Term &t)
bool check_term_ActionRenameRule(const Term &t)
bool check_rule_ActionRenameRule(const Term &t)
bool check_rule_PBExpr(const Term &t)
bool check_term_StateNot(const Term &t)
bool check_term_PRESFalse(const Term &t)
bool check_rule_UntypedMultiAction(const Term &t)
bool check_term_OpId(const Term &t)
bool check_term_Distribution(const Term &t)
bool check_term_ActNot(const Term &t)
bool check_term_PRESEqNInf(const Term &t)
bool check_term_UntypedSortsPossible(const Term &t)
bool check_rule_UntypedDataParameter(const Term &t)
bool check_term_Hide(const Term &t)
bool check_rule_PREqnSpec(const Term &t)
bool check_rule_TimedMultAct(const Term &t)
bool check_term_Merge(const Term &t)
bool check_rule_PropVarInst(const Term &t)
bool check_term_Exists(const Term &t)
bool check_term_SetComp(const Term &t)
bool check_term_ActOr(const Term &t)
bool check_term_StructProj(const Term &t)
bool check_term_PRESMinus(const Term &t)
bool check_rule_MultAct(const Term &t)
bool check_term_SortList(const Term &t)
bool check_term_PBEqnSpec(const Term &t)
bool check_rule_LinearProcessInit(const Term &t)
bool check_rule_PBInit(const Term &t)
bool check_term_IfThenElse(const Term &t)
bool check_term_PBESAnd(const Term &t)
bool check_rule_ProcInit(const Term &t)
bool check_term_PBESFalse(const Term &t)
bool check_rule_StructCons(const Term &t)
bool check_term_PRESPlus(const Term &t)
bool check_rule_OpId(const Term &t)
bool check_term_PropVarDecl(const Term &t)
bool check_term_SortFSet(const Term &t)
bool check_term_PRESCondSm(const Term &t)
bool check_term_Block(const Term &t)
bool check_term_StateExists(const Term &t)
bool check_term_ActionRenameRules(const Term &t)
bool check_term_StateConstantMultiplyAlt(const Term &t)
bool check_term_DataAppl(const Term &t)
bool check_term_RegSeq(const Term &t)
bool check_term_PRESImp(const Term &t)
bool check_term_RegAlt(const Term &t)
bool check_rule_PRInit(const Term &t)
apply_builder< Builder > make_apply_builder()
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1(const Function &f)
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
apply_builder_arg1< Builder, Arg1 > make_apply_builder_arg1(const Arg1 &arg1)
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
data_expression parse_data_expression(const std::string &text)
data_specification parse_data_specification_new(const std::string &text)
variable_list parse_variable_declaration_list(const std::string &text)
variable_list parse_variables(const std::string &text)
sort_expression parse_sort_expression(const std::string &text)
Namespace for system defined sort bool_.
const basic_sort & bool_()
Constructor for sort expression Bool.
std::string pp(const data::structured_sort_constructor_argument &x, bool arg0)
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
data::data_equation_list normalize_sorts(const data::data_equation_list &x, const data::sort_specification &sortspec)
std::string pp(const data::exists &x, bool arg0)
std::string pp(const data::untyped_identifier_assignment &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const basic_sort &x)
std::set< data::variable > find_all_variables(const data::data_expression_list &x)
std::string pp(const data::list_container &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const data::data_expression &x)
data::data_equation translate_user_notation(const data::data_equation &x)
bool is_application(const data_expression &t)
Returns true if the term t is an application.
void make_basic_sort(atermpp::aterm &t, const ARGUMENTS &... args)
void swap(basic_sort &t1, basic_sort &t2) noexcept
\brief swap overload
std::string pp(const data::container_type &x, bool arg0)
std::set< data::variable > find_all_variables(const data::data_expression &x)
bool is_where_clause(const atermpp::aterm &x)
Returns true if the term t is a where clause.
std::string pp(const data::set_container &x, bool arg0)
bool is_untyped_possible_sorts(const atermpp::aterm &x)
Returns true if the term t is an expression for multiple possible sorts.
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
std::string pp(const data::untyped_set_or_bag_comprehension_binder &x, bool arg0)
data::data_expression translate_user_notation(const data::data_expression &x)
std::string pp(const data::sort_expression_vector &x, bool arg0)
std::string pp(const data::untyped_sort &x, bool arg0)
std::string pp(const data::data_equation &x, bool arg0)
std::string pp(const data::forall &x, bool arg0)
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
std::string pp(const data::assignment_list &x, bool arg0)
std::string pp(const data::untyped_identifier &x, bool arg0)
std::string pp(const data::function_symbol_list &x, bool arg0)
bool is_untyped_identifier(const atermpp::aterm &x)
Returns true if the term t is an identifier.
std::string pp(const data::lambda_binder &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const alias &x)
std::set< data::variable > find_all_variables(const data::function_symbol &x)
std::string pp(const data::application &x, bool arg0)
std::string pp(const data::function_sort &x, bool arg0)
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const data::abstraction &x, bool arg0)
std::string pp(const data::bag_comprehension_binder &x, bool arg0)
std::string pp(const data::set_comprehension_binder &x, bool arg0)
std::string pp(const data::assignment &x, bool arg0)
std::string pp(const data::structured_sort &x, bool arg0)
std::string pp(const data::basic_sort &x, bool arg0)
std::string pp(const data::exists_binder &x, bool arg0)
std::string pp(const data::bag_comprehension &x, bool arg0)
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
std::string pp(const data::variable &x, bool arg0)
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
bool is_untyped_sort_variable(const atermpp::aterm &x)
std::string pp(const data::where_clause &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
std::string pp(const data::bag_container &x, bool arg0)
std::string pp(const data::alias &x, bool arg0)
std::set< data::variable > find_free_variables(const data::data_expression &x)
void swap(sort_expression &t1, sort_expression &t2) noexcept
\brief swap overload
std::set< data::variable > find_all_variables(const data::variable_list &x)
bool is_untyped_set_or_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set/bag comprehension.
void swap(alias &t1, alias &t2) noexcept
\brief swap overload
bool is_assignment(const atermpp::aterm &x)
std::string pp(const data::structured_sort_constructor &x, bool arg0)
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
std::string pp(const data::data_specification &x, bool arg0)
std::string pp(const data::data_equation_list &x, bool arg0)
std::string pp(const data::fset_container &x, bool arg0)
std::string pp(const data::sort_expression &x, bool arg0)
std::string pp(const data::untyped_set_or_bag_comprehension &x, bool arg0)
std::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
std::string pp(const data::variable_list &x, bool arg0)
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
std::set< data::variable > find_free_variables(const data::data_expression_list &x)
std::string pp(const data::data_expression &x, bool arg0)
std::string pp(const data::lambda &x, bool arg0)
bool is_bag_comprehension(const atermpp::aterm &x)
Returns true if the term t is a bag comprehension.
std::string pp(const data::fbag_container &x, bool arg0)
bool is_set_comprehension(const atermpp::aterm &x)
Returns true if the term t is a set comprehension.
std::string pp(const data::structured_sort_constructor_list &x, bool arg0)
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
std::string pp(const data::container_sort &x, bool arg0)
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
data::data_expression normalize_sorts(const data::data_expression &x, const data::sort_specification &sortspec)
std::string pp(const data::untyped_sort_variable &x, bool arg0)
std::string pp(const data::untyped_data_parameter &x, bool arg0)
std::string pp(const data::binder_type &x, bool arg0)
bool is_lambda(const atermpp::aterm &x)
Returns true if the term t is a lambda abstraction.
bool is_untyped_identifier_assignment(const atermpp::aterm &x)
bool is_alias(const atermpp::aterm &x)
std::set< data::variable > find_all_variables(const data::variable &x)
std::set< core::identifier_string > find_identifiers(const data::variable_list &x)
std::ostream & operator<<(std::ostream &out, const sort_expression &x)
bool search_variable(const data::data_expression &x, const data::variable &v)
std::string pp(const data::sort_expression_list &x, bool arg0)
std::string pp(const data::forall_binder &x, bool arg0)
std::string pp(const data::untyped_possible_sorts &x, bool arg0)
std::string pp(const data::function_symbol &x, bool arg0)
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
std::string pp(const data::machine_number &x, bool arg0)
std::string pp(const data::assignment_expression &x, bool arg0)
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
bool is_sort_expression(const atermpp::aterm &x)
Test for a sort_expression expression.
std::string pp(const data::set_comprehension &x, bool arg0)
std::string pp(const data::data_expression_list &x, bool arg0)
expression builder that visits all sub expressions
static const atermpp::aterm SortExpr
static const atermpp::aterm SortId
static const atermpp::aterm SortRef
void apply(T &result, const argument_type &x)
update_apply_builder(const Function &f)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::data_equation &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::structured_sort_constructor_argument &x)
void apply(T &result, const data::container_sort &x)
void apply(T &result, const data::alias &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::untyped_possible_sorts &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::basic_sort &x)
void apply(T &result, const data::data_equation &x)
void apply(T &result, const data::untyped_sort &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::structured_sort &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::function_sort &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::structured_sort_constructor &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::sort_expression &x)
void apply(T &result, const data::untyped_sort_variable &x)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::abstraction &x)
void apply(T &result, const data::application &x)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::untyped_identifier &x)
void apply(T &result, const data::data_expression &x)
void apply(T &result, const data::assignment_expression &x)
void apply(T &result, const data::where_clause &x)
void apply(T &result, const data::forall &x)
void apply(T &result, const data::function_symbol &x)
void apply(T &result, const data::exists &x)
void apply(T &result, const data::lambda &x)
void apply(T &result, const data::variable &x)
void apply(T &result, const data::assignment &x)
void apply(T &result, const data::untyped_identifier_assignment &x)
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
void apply(T &result, const data::set_comprehension &x)
void apply(T &result, const data::bag_comprehension &x)
void apply(T &result, const data::machine_number &x)
void apply(T &result, const data::data_equation &x)
data_expression_actions(const core::parser &parser_)
data::data_expression parse_DataExpr(const core::parse_node &node) const
data_specification_actions(const core::parser &parser_)
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
normalize_sorts_function(const sort_specification &sort_spec)
sort_expression operator()(const sort_expression &e) const
Normalise sorts.
const std::map< sort_expression, sort_expression > & m_normalised_aliases
data::sort_expression parse_SortExpr(const core::parse_node &node, data::sort_expression_list *product=nullptr) const
data_specification construct_data_specification() const
std::size_t operator()(const mcrl2::data::sort_expression &x) const