soundness_checks.h File Reference

Add your file description here. More...

Go to the source code of this file.

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::core
namespace	mcrl2::core::detail

Functions
template<typename Term , typename CheckFunction >
bool	mcrl2::core::detail::check_term_argument (const Term &t, CheckFunction f)
template<typename Term , typename CheckFunction >
bool	mcrl2::core::detail::check_list_argument (const Term &t, CheckFunction f, unsigned int minimum_size)
template<typename Term >
bool	mcrl2::core::detail::check_rule_String (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_StringOrEmpty (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_Number (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_DataExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_DataAppl (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_SortExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_SortId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_SortConsType (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_StructCons (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_StructProj (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_DataVarId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_OpId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_UntypedDataParameter (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_BindingOperator (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_WhrDecl (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_DataVarIdInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_UntypedIdentifierAssignment (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_DataSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_SortSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ConsSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_MapSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_DataEqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_SortDecl (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_DataEqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_MultAct (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_TimedMultAct (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_UntypedMultiAction (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_Action (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ActId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ProcExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ProcVarId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_MultActName (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_RenameExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_CommExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ProcSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ActSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_GlobVarSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ProcEqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ProcEqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_MultActOrDelta (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ProcInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_Distribution (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_LinProcSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_LinearProcess (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_LinearProcessSummand (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_LinearProcessInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_StateFrm (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_RegFrm (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ActFrm (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ParamIdOrAction (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ActionRenameRules (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ActionRenameRule (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ActionRenameRuleRHS (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_ActionRenameSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PBES (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PBEqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PBInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PBEqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_FixPoint (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PropVarDecl (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PBExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PropVarInst (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PRES (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PREqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PRInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PREqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_rule_PRExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortCons (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortStruct (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortArrow (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedSortUnknown (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedSortsPossible (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedSortVariable (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortList (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortSet (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortBag (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortFSet (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortFBag (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StructCons (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StructProj (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Binder (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Whr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedIdentifier (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_DataVarId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_OpId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedDataParameter (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Forall (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Exists (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SetComp (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_BagComp (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Lambda (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedSetBagComp (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_DataVarIdInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedIdentifierAssignment (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_DataSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ConsSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_MapSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_DataEqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_SortRef (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_DataEqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_MultAct (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_TimedMultAct (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedMultiAction (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Action (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Process (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ProcessAssignment (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Delta (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Tau (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Sum (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Block (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Hide (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Rename (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Comm (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Allow (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Sync (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_AtTime (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Seq (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_IfThen (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_IfThenElse (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_BInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Merge (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_LMerge (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Choice (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StochasticOperator (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedProcessAssignment (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ProcVarId (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_MultActName (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_RenameExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_CommExpr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ProcSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_GlobVarSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ProcEqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ProcEqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ProcessInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Distribution (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_LinProcSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_LinearProcess (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_LinearProcessSummand (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_LinearProcessInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateTrue (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateFalse (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateNot (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateMinus (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateAnd (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateOr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateImp (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StatePlus (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateConstantMultiply (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateConstantMultiplyAlt (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateForall (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateExists (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateInfimum (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateSupremum (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateSum (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateMust (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateMay (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateYaled (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateYaledTimed (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateDelay (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateDelayTimed (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateVar (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateNu (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_StateMu (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_RegNil (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_RegSeq (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_RegAlt (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_RegTrans (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_RegTransOrNil (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_UntypedRegFrm (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActTrue (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActFalse (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActNot (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActAnd (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActOr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActImp (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActForall (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActExists (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActAt (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActMultAct (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActionRenameRules (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActionRenameRule (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_ActionRenameSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBES (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBEqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBEqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Mu (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_Nu (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PropVarDecl (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESTrue (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESFalse (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESNot (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESAnd (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESOr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESImp (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESForall (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PBESExists (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PropVarInst (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRES (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PREqnSpec (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRInit (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PREqn (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESTrue (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESFalse (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESMinus (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESAnd (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESOr (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESImp (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESPlus (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESConstantMultiply (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESConstantMultiplyAlt (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESInfimum (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESSupremum (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESSum (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESEqInf (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESEqNInf (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESCondSm (const Term &t)
template<typename Term >
bool	mcrl2::core::detail::check_term_PRESCondEq (const Term &t)

Detailed Description

Add your file description here.

Definition in file soundness_checks.h.