mCRL2
Loading...
Searching...
No Matches
soundness_checks.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/core/detail/soundness_checks.h
10/// \brief Add your file description here.
11
12#ifndef MCRL2_CORE_DETAIL_SOUNDNESS_CHECKS_H
13#define MCRL2_CORE_DETAIL_SOUNDNESS_CHECKS_H
14
15// This file contains soundness checks for LPS terms.
16// N.B. This file is automatically generated!
17
18#include "mcrl2/atermpp/concepts.h"
19#include "mcrl2/atermpp/aterm_string.h"
20#include "mcrl2/core/detail/function_symbols.h"
21
22namespace mcrl2::core::detail
23{
24
25// checks
26// 1) if term t satisfies the predicate f
27template <atermpp::IsATerm Term, typename CheckFunction>
28bool check_term_argument(const Term& t, CheckFunction f)
29{
30 return f(t);
31}
32
33// checks
34// 1) if term t is a list,
35// 2) if the list has the proper minimum size
36// 3) if all elements of the list satisfy the predicate f
37template <atermpp::IsATerm Term, typename CheckFunction>
38bool check_list_argument(const Term& t, CheckFunction f, unsigned int minimum_size)
39{
40 const atermpp::aterm& term(t);
41 if (!t.type_is_list())
42 {
43 return false;
44 }
45 const atermpp::aterm_list& l = atermpp::down_cast<atermpp::aterm_list>(term);
46 if (l.size() < minimum_size)
47 {
48 return false;
49 }
50 for (const auto& x: l)
51 {
52 if (!f(x))
53 {
54 return false;
55 }
56 }
57 return true;
58}
59
60template <atermpp::IsATerm Term>
61bool check_rule_String(const Term& t)
62{
63 const atermpp::aterm& term(t);
64 if (!term.type_is_appl())
65 {
66 return false;
67 }
68 if (term.size() > 0)
69 {
70 return false;
71 }
72 if (term == atermpp::empty_string())
73 {
74 return false;
75 }
76 return true;
77}
78
79template <atermpp::IsATerm Term>
80bool check_rule_StringOrEmpty(const Term& t)
81{
82 const atermpp::aterm& term(t);
83 if (!term.type_is_appl())
84 {
85 return false;
86 }
87 return term.size() <= 0;
88}
89
90template <atermpp::IsATerm Term>
91bool check_rule_Number(const Term& t)
92{
93 const atermpp::aterm& term(t);
94 return term.type_is_int();
95}
96
97template <atermpp::IsATerm Term> bool check_rule_DataExpr(const Term& t);
98
99// DataAppl(DataExpr, DataExpr+)
100template <atermpp::IsATerm Term>
101bool check_term_DataAppl(const Term& t)
102{
103#ifndef MCRL2_NO_SOUNDNESS_CHECKS
104 // check the type of the term
105 const atermpp::aterm& term(t);
106 if (term.type_is_int())
107 {
108 return true;
109 }
110 if (!term.type_is_appl())
111 {
112 return false;
113 }
114 if (!gsIsDataAppl(term))
115 {
116 return false;
117 }
118#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
119 for (const atermpp::aterm& child : term)
120 {
121 if (!check_term_argument(child, check_rule_DataExpr<atermpp::aterm>))
122 {
123 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
124 return false;
125 }
126 }
127#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
128
129#endif // MCRL2_NO_SOUNDNESS_CHECKS
130 return true;
131}
132
133//--- start generated code ---//
134template <atermpp::IsATerm Term> bool check_rule_SortExpr(const Term& t);
135template <atermpp::IsATerm Term> bool check_rule_SortId(const Term& t);
136template <atermpp::IsATerm Term> bool check_rule_SortConsType(const Term& t);
137template <atermpp::IsATerm Term> bool check_rule_StructCons(const Term& t);
138template <atermpp::IsATerm Term> bool check_rule_StructProj(const Term& t);
139template <atermpp::IsATerm Term> bool check_rule_DataExpr(const Term& t);
140template <atermpp::IsATerm Term> bool check_rule_DataVarId(const Term& t);
141template <atermpp::IsATerm Term> bool check_rule_OpId(const Term& t);
142template <atermpp::IsATerm Term> bool check_rule_UntypedDataParameter(const Term& t);
143template <atermpp::IsATerm Term> bool check_rule_BindingOperator(const Term& t);
144template <atermpp::IsATerm Term> bool check_rule_WhrDecl(const Term& t);
145template <atermpp::IsATerm Term> bool check_rule_DataVarIdInit(const Term& t);
146template <atermpp::IsATerm Term> bool check_rule_UntypedIdentifierAssignment(const Term& t);
147template <atermpp::IsATerm Term> bool check_rule_DataSpec(const Term& t);
148template <atermpp::IsATerm Term> bool check_rule_SortSpec(const Term& t);
149template <atermpp::IsATerm Term> bool check_rule_ConsSpec(const Term& t);
150template <atermpp::IsATerm Term> bool check_rule_MapSpec(const Term& t);
151template <atermpp::IsATerm Term> bool check_rule_DataEqnSpec(const Term& t);
152template <atermpp::IsATerm Term> bool check_rule_SortDecl(const Term& t);
153template <atermpp::IsATerm Term> bool check_rule_DataEqn(const Term& t);
154template <atermpp::IsATerm Term> bool check_rule_MultAct(const Term& t);
155template <atermpp::IsATerm Term> bool check_rule_TimedMultAct(const Term& t);
156template <atermpp::IsATerm Term> bool check_rule_UntypedMultiAction(const Term& t);
157template <atermpp::IsATerm Term> bool check_rule_Action(const Term& t);
158template <atermpp::IsATerm Term> bool check_rule_ActId(const Term& t);
159template <atermpp::IsATerm Term> bool check_rule_ProcExpr(const Term& t);
160template <atermpp::IsATerm Term> bool check_rule_ProcVarId(const Term& t);
161template <atermpp::IsATerm Term> bool check_rule_MultActName(const Term& t);
162template <atermpp::IsATerm Term> bool check_rule_RenameExpr(const Term& t);
163template <atermpp::IsATerm Term> bool check_rule_CommExpr(const Term& t);
164template <atermpp::IsATerm Term> bool check_rule_ProcSpec(const Term& t);
165template <atermpp::IsATerm Term> bool check_rule_ActSpec(const Term& t);
166template <atermpp::IsATerm Term> bool check_rule_GlobVarSpec(const Term& t);
167template <atermpp::IsATerm Term> bool check_rule_ProcEqnSpec(const Term& t);
168template <atermpp::IsATerm Term> bool check_rule_ProcEqn(const Term& t);
169template <atermpp::IsATerm Term> bool check_rule_MultActOrDelta(const Term& t);
170template <atermpp::IsATerm Term> bool check_rule_ProcInit(const Term& t);
171template <atermpp::IsATerm Term> bool check_rule_Distribution(const Term& t);
172template <atermpp::IsATerm Term> bool check_rule_LinProcSpec(const Term& t);
173template <atermpp::IsATerm Term> bool check_rule_LinearProcess(const Term& t);
174template <atermpp::IsATerm Term> bool check_rule_LinearProcessSummand(const Term& t);
175template <atermpp::IsATerm Term> bool check_rule_LinearProcessInit(const Term& t);
176template <atermpp::IsATerm Term> bool check_rule_StateFrm(const Term& t);
177template <atermpp::IsATerm Term> bool check_rule_RegFrm(const Term& t);
178template <atermpp::IsATerm Term> bool check_rule_ActFrm(const Term& t);
179template <atermpp::IsATerm Term> bool check_rule_ParamIdOrAction(const Term& t);
180template <atermpp::IsATerm Term> bool check_rule_ActionRenameRules(const Term& t);
181template <atermpp::IsATerm Term> bool check_rule_ActionRenameRule(const Term& t);
182template <atermpp::IsATerm Term> bool check_rule_ActionRenameRuleRHS(const Term& t);
183template <atermpp::IsATerm Term> bool check_rule_ActionRenameSpec(const Term& t);
184template <atermpp::IsATerm Term> bool check_rule_PBES(const Term& t);
185template <atermpp::IsATerm Term> bool check_rule_PBEqnSpec(const Term& t);
186template <atermpp::IsATerm Term> bool check_rule_PBInit(const Term& t);
187template <atermpp::IsATerm Term> bool check_rule_PBEqn(const Term& t);
188template <atermpp::IsATerm Term> bool check_rule_FixPoint(const Term& t);
189template <atermpp::IsATerm Term> bool check_rule_PropVarDecl(const Term& t);
190template <atermpp::IsATerm Term> bool check_rule_PBExpr(const Term& t);
191template <atermpp::IsATerm Term> bool check_rule_PropVarInst(const Term& t);
192template <atermpp::IsATerm Term> bool check_rule_PRES(const Term& t);
193template <atermpp::IsATerm Term> bool check_rule_PREqnSpec(const Term& t);
194template <atermpp::IsATerm Term> bool check_rule_PRInit(const Term& t);
195template <atermpp::IsATerm Term> bool check_rule_PREqn(const Term& t);
196template <atermpp::IsATerm Term> bool check_rule_PRExpr(const Term& t);
197template <atermpp::IsATerm Term> bool check_term_SortCons(const Term& t);
198template <atermpp::IsATerm Term> bool check_term_SortStruct(const Term& t);
199template <atermpp::IsATerm Term> bool check_term_SortArrow(const Term& t);
200template <atermpp::IsATerm Term> bool check_term_UntypedSortUnknown(const Term& t);
201template <atermpp::IsATerm Term> bool check_term_UntypedSortsPossible(const Term& t);
202template <atermpp::IsATerm Term> bool check_term_UntypedSortVariable(const Term& t);
203template <atermpp::IsATerm Term> bool check_term_SortId(const Term& t);
204template <atermpp::IsATerm Term> bool check_term_SortList(const Term& t);
205template <atermpp::IsATerm Term> bool check_term_SortSet(const Term& t);
206template <atermpp::IsATerm Term> bool check_term_SortBag(const Term& t);
207template <atermpp::IsATerm Term> bool check_term_SortFSet(const Term& t);
208template <atermpp::IsATerm Term> bool check_term_SortFBag(const Term& t);
209template <atermpp::IsATerm Term> bool check_term_StructCons(const Term& t);
210template <atermpp::IsATerm Term> bool check_term_StructProj(const Term& t);
211template <atermpp::IsATerm Term> bool check_term_Binder(const Term& t);
212template <atermpp::IsATerm Term> bool check_term_Whr(const Term& t);
213template <atermpp::IsATerm Term> bool check_term_UntypedIdentifier(const Term& t);
214template <atermpp::IsATerm Term> bool check_term_DataVarId(const Term& t);
215template <atermpp::IsATerm Term> bool check_term_OpId(const Term& t);
216template <atermpp::IsATerm Term> bool check_term_UntypedDataParameter(const Term& t);
217template <atermpp::IsATerm Term> bool check_term_Forall(const Term& t);
218template <atermpp::IsATerm Term> bool check_term_Exists(const Term& t);
219template <atermpp::IsATerm Term> bool check_term_SetComp(const Term& t);
220template <atermpp::IsATerm Term> bool check_term_BagComp(const Term& t);
221template <atermpp::IsATerm Term> bool check_term_Lambda(const Term& t);
222template <atermpp::IsATerm Term> bool check_term_UntypedSetBagComp(const Term& t);
223template <atermpp::IsATerm Term> bool check_term_DataVarIdInit(const Term& t);
224template <atermpp::IsATerm Term> bool check_term_UntypedIdentifierAssignment(const Term& t);
225template <atermpp::IsATerm Term> bool check_term_DataSpec(const Term& t);
226template <atermpp::IsATerm Term> bool check_term_SortSpec(const Term& t);
227template <atermpp::IsATerm Term> bool check_term_ConsSpec(const Term& t);
228template <atermpp::IsATerm Term> bool check_term_MapSpec(const Term& t);
229template <atermpp::IsATerm Term> bool check_term_DataEqnSpec(const Term& t);
230template <atermpp::IsATerm Term> bool check_term_SortRef(const Term& t);
231template <atermpp::IsATerm Term> bool check_term_DataEqn(const Term& t);
232template <atermpp::IsATerm Term> bool check_term_MultAct(const Term& t);
233template <atermpp::IsATerm Term> bool check_term_TimedMultAct(const Term& t);
234template <atermpp::IsATerm Term> bool check_term_UntypedMultiAction(const Term& t);
235template <atermpp::IsATerm Term> bool check_term_Action(const Term& t);
236template <atermpp::IsATerm Term> bool check_term_ActId(const Term& t);
237template <atermpp::IsATerm Term> bool check_term_Process(const Term& t);
238template <atermpp::IsATerm Term> bool check_term_ProcessAssignment(const Term& t);
239template <atermpp::IsATerm Term> bool check_term_Delta(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);
242template <atermpp::IsATerm Term> bool check_term_Block(const Term& t);
243template <atermpp::IsATerm Term> bool check_term_Hide(const Term& t);
244template <atermpp::IsATerm Term> bool check_term_Rename(const Term& t);
245template <atermpp::IsATerm Term> bool check_term_Comm(const Term& t);
246template <atermpp::IsATerm Term> bool check_term_Allow(const Term& t);
247template <atermpp::IsATerm Term> bool check_term_Sync(const Term& t);
248template <atermpp::IsATerm Term> bool check_term_AtTime(const Term& t);
249template <atermpp::IsATerm Term> bool check_term_Seq(const Term& t);
250template <atermpp::IsATerm Term> bool check_term_IfThen(const Term& t);
251template <atermpp::IsATerm Term> bool check_term_IfThenElse(const Term& t);
252template <atermpp::IsATerm Term> bool check_term_BInit(const Term& t);
253template <atermpp::IsATerm Term> bool check_term_Merge(const Term& t);
254template <atermpp::IsATerm Term> bool check_term_LMerge(const Term& t);
255template <atermpp::IsATerm Term> bool check_term_Choice(const Term& t);
256template <atermpp::IsATerm Term> bool check_term_StochasticOperator(const Term& t);
257template <atermpp::IsATerm Term> bool check_term_UntypedProcessAssignment(const Term& t);
258template <atermpp::IsATerm Term> bool check_term_ProcVarId(const Term& t);
259template <atermpp::IsATerm Term> bool check_term_MultActName(const Term& t);
260template <atermpp::IsATerm Term> bool check_term_RenameExpr(const Term& t);
261template <atermpp::IsATerm Term> bool check_term_CommExpr(const Term& t);
262template <atermpp::IsATerm Term> bool check_term_ProcSpec(const Term& t);
263template <atermpp::IsATerm Term> bool check_term_ActSpec(const Term& t);
264template <atermpp::IsATerm Term> bool check_term_GlobVarSpec(const Term& t);
265template <atermpp::IsATerm Term> bool check_term_ProcEqnSpec(const Term& t);
266template <atermpp::IsATerm Term> bool check_term_ProcEqn(const Term& t);
267template <atermpp::IsATerm Term> bool check_term_ProcessInit(const Term& t);
268template <atermpp::IsATerm Term> bool check_term_Distribution(const Term& t);
269template <atermpp::IsATerm Term> bool check_term_LinProcSpec(const Term& t);
270template <atermpp::IsATerm Term> bool check_term_LinearProcess(const Term& t);
271template <atermpp::IsATerm Term> bool check_term_LinearProcessSummand(const Term& t);
272template <atermpp::IsATerm Term> bool check_term_LinearProcessInit(const Term& t);
273template <atermpp::IsATerm Term> bool check_term_StateTrue(const Term& t);
274template <atermpp::IsATerm Term> bool check_term_StateFalse(const Term& t);
275template <atermpp::IsATerm Term> bool check_term_StateNot(const Term& t);
276template <atermpp::IsATerm Term> bool check_term_StateMinus(const Term& t);
277template <atermpp::IsATerm Term> bool check_term_StateAnd(const Term& t);
278template <atermpp::IsATerm Term> bool check_term_StateOr(const Term& t);
279template <atermpp::IsATerm Term> bool check_term_StateImp(const Term& t);
280template <atermpp::IsATerm Term> bool check_term_StatePlus(const Term& t);
281template <atermpp::IsATerm Term> bool check_term_StateConstantMultiply(const Term& t);
282template <atermpp::IsATerm Term> bool check_term_StateConstantMultiplyAlt(const Term& t);
283template <atermpp::IsATerm Term> bool check_term_StateForall(const Term& t);
284template <atermpp::IsATerm Term> bool check_term_StateExists(const Term& t);
285template <atermpp::IsATerm Term> bool check_term_StateInfimum(const Term& t);
286template <atermpp::IsATerm Term> bool check_term_StateSupremum(const Term& t);
287template <atermpp::IsATerm Term> bool check_term_StateSum(const Term& t);
288template <atermpp::IsATerm Term> bool check_term_StateMust(const Term& t);
289template <atermpp::IsATerm Term> bool check_term_StateMay(const Term& t);
290template <atermpp::IsATerm Term> bool check_term_StateYaled(const Term& t);
291template <atermpp::IsATerm Term> bool check_term_StateYaledTimed(const Term& t);
292template <atermpp::IsATerm Term> bool check_term_StateDelay(const Term& t);
293template <atermpp::IsATerm Term> bool check_term_StateDelayTimed(const Term& t);
294template <atermpp::IsATerm Term> bool check_term_StateVar(const Term& t);
295template <atermpp::IsATerm Term> bool check_term_StateNu(const Term& t);
296template <atermpp::IsATerm Term> bool check_term_StateMu(const Term& t);
297template <atermpp::IsATerm Term> bool check_term_RegNil(const Term& t);
298template <atermpp::IsATerm Term> bool check_term_RegSeq(const Term& t);
299template <atermpp::IsATerm Term> bool check_term_RegAlt(const Term& t);
300template <atermpp::IsATerm Term> bool check_term_RegTrans(const Term& t);
301template <atermpp::IsATerm Term> bool check_term_RegTransOrNil(const Term& t);
302template <atermpp::IsATerm Term> bool check_term_UntypedRegFrm(const Term& t);
303template <atermpp::IsATerm Term> bool check_term_ActTrue(const Term& t);
304template <atermpp::IsATerm Term> bool check_term_ActFalse(const Term& t);
305template <atermpp::IsATerm Term> bool check_term_ActNot(const Term& t);
306template <atermpp::IsATerm Term> bool check_term_ActAnd(const Term& t);
307template <atermpp::IsATerm Term> bool check_term_ActOr(const Term& t);
308template <atermpp::IsATerm Term> bool check_term_ActImp(const Term& t);
309template <atermpp::IsATerm Term> bool check_term_ActForall(const Term& t);
310template <atermpp::IsATerm Term> bool check_term_ActExists(const Term& t);
311template <atermpp::IsATerm Term> bool check_term_ActAt(const Term& t);
312template <atermpp::IsATerm Term> bool check_term_ActMultAct(const Term& t);
313template <atermpp::IsATerm Term> bool check_term_ActionRenameRules(const Term& t);
314template <atermpp::IsATerm Term> bool check_term_ActionRenameRule(const Term& t);
315template <atermpp::IsATerm Term> bool check_term_ActionRenameSpec(const Term& t);
316template <atermpp::IsATerm Term> bool check_term_PBES(const Term& t);
317template <atermpp::IsATerm Term> bool check_term_PBEqnSpec(const Term& t);
318template <atermpp::IsATerm Term> bool check_term_PBInit(const Term& t);
319template <atermpp::IsATerm Term> bool check_term_PBEqn(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);
322template <atermpp::IsATerm Term> bool check_term_PropVarDecl(const Term& t);
323template <atermpp::IsATerm Term> bool check_term_PBESTrue(const Term& t);
324template <atermpp::IsATerm Term> bool check_term_PBESFalse(const Term& t);
325template <atermpp::IsATerm Term> bool check_term_PBESNot(const Term& t);
326template <atermpp::IsATerm Term> bool check_term_PBESAnd(const Term& t);
327template <atermpp::IsATerm Term> bool check_term_PBESOr(const Term& t);
328template <atermpp::IsATerm Term> bool check_term_PBESImp(const Term& t);
329template <atermpp::IsATerm Term> bool check_term_PBESForall(const Term& t);
330template <atermpp::IsATerm Term> bool check_term_PBESExists(const Term& t);
331template <atermpp::IsATerm Term> bool check_term_PropVarInst(const Term& t);
332template <atermpp::IsATerm Term> bool check_term_PRES(const Term& t);
333template <atermpp::IsATerm Term> bool check_term_PREqnSpec(const Term& t);
334template <atermpp::IsATerm Term> bool check_term_PRInit(const Term& t);
335template <atermpp::IsATerm Term> bool check_term_PREqn(const Term& t);
336template <atermpp::IsATerm Term> bool check_term_PRESTrue(const Term& t);
337template <atermpp::IsATerm Term> bool check_term_PRESFalse(const Term& t);
338template <atermpp::IsATerm Term> bool check_term_PRESMinus(const Term& t);
339template <atermpp::IsATerm Term> bool check_term_PRESAnd(const Term& t);
340template <atermpp::IsATerm Term> bool check_term_PRESOr(const Term& t);
341template <atermpp::IsATerm Term> bool check_term_PRESImp(const Term& t);
342template <atermpp::IsATerm Term> bool check_term_PRESPlus(const Term& t);
343template <atermpp::IsATerm Term> bool check_term_PRESConstantMultiply(const Term& t);
344template <atermpp::IsATerm Term> bool check_term_PRESConstantMultiplyAlt(const Term& t);
345template <atermpp::IsATerm Term> bool check_term_PRESInfimum(const Term& t);
346template <atermpp::IsATerm Term> bool check_term_PRESSupremum(const Term& t);
347template <atermpp::IsATerm Term> bool check_term_PRESSum(const Term& t);
348template <atermpp::IsATerm Term> bool check_term_PRESEqInf(const Term& t);
349template <atermpp::IsATerm Term> bool check_term_PRESEqNInf(const Term& t);
350template <atermpp::IsATerm Term> bool check_term_PRESCondSm(const Term& t);
351template <atermpp::IsATerm Term> bool check_term_PRESCondEq(const Term& t);
352
353template <atermpp::IsATerm Term>
354bool check_rule_SortExpr([[maybe_unused]] const Term& t)
355{
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);
364#else
365 return true;
366#endif // MCRL2_NO_SOUNDNESS_CHECKS
367}
368
369template <atermpp::IsATerm Term>
370bool check_rule_SortId([[maybe_unused]] const Term& t)
371{
372#ifndef MCRL2_NO_SOUNDNESS_CHECKS
373 return check_term_SortId(t);
374#else
375 return true;
376#endif // MCRL2_NO_SOUNDNESS_CHECKS
377}
378
379template <atermpp::IsATerm Term>
381{
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);
388#else
389 return true;
390#endif // MCRL2_NO_SOUNDNESS_CHECKS
391}
392
393template <atermpp::IsATerm Term>
394bool check_rule_StructCons([[maybe_unused]] const Term& t)
395{
396#ifndef MCRL2_NO_SOUNDNESS_CHECKS
397 return check_term_StructCons(t);
398#else
399 return true;
400#endif // MCRL2_NO_SOUNDNESS_CHECKS
401}
402
403template <atermpp::IsATerm Term>
404bool check_rule_StructProj([[maybe_unused]] const Term& t)
405{
406#ifndef MCRL2_NO_SOUNDNESS_CHECKS
407 return check_term_StructProj(t);
408#else
409 return true;
410#endif // MCRL2_NO_SOUNDNESS_CHECKS
411}
412
413template <atermpp::IsATerm Term>
414bool check_rule_DataExpr([[maybe_unused]] const Term& t)
415{
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)
421 || check_term_Whr(t)
422 || check_term_UntypedIdentifier(t);
423#else
424 return true;
425#endif // MCRL2_NO_SOUNDNESS_CHECKS
426}
427
428template <atermpp::IsATerm Term>
429bool check_rule_DataVarId([[maybe_unused]] const Term& t)
430{
431#ifndef MCRL2_NO_SOUNDNESS_CHECKS
432 return check_term_DataVarId(t);
433#else
434 return true;
435#endif // MCRL2_NO_SOUNDNESS_CHECKS
436}
437
438template <atermpp::IsATerm Term>
439bool check_rule_OpId([[maybe_unused]] const Term& t)
440{
441#ifndef MCRL2_NO_SOUNDNESS_CHECKS
442 return check_term_OpId(t);
443#else
444 return true;
445#endif // MCRL2_NO_SOUNDNESS_CHECKS
446}
447
448template <atermpp::IsATerm Term>
450{
451#ifndef MCRL2_NO_SOUNDNESS_CHECKS
452 return check_term_UntypedDataParameter(t);
453#else
454 return true;
455#endif // MCRL2_NO_SOUNDNESS_CHECKS
456}
457
458template <atermpp::IsATerm Term>
460{
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);
468#else
469 return true;
470#endif // MCRL2_NO_SOUNDNESS_CHECKS
471}
472
473template <atermpp::IsATerm Term>
474bool check_rule_WhrDecl([[maybe_unused]] const Term& t)
475{
476#ifndef MCRL2_NO_SOUNDNESS_CHECKS
477 return check_rule_DataVarIdInit(t)
478 || check_rule_UntypedIdentifierAssignment(t);
479#else
480 return true;
481#endif // MCRL2_NO_SOUNDNESS_CHECKS
482}
483
484template <atermpp::IsATerm Term>
486{
487#ifndef MCRL2_NO_SOUNDNESS_CHECKS
488 return check_term_DataVarIdInit(t);
489#else
490 return true;
491#endif // MCRL2_NO_SOUNDNESS_CHECKS
492}
493
494template <atermpp::IsATerm Term>
496{
497#ifndef MCRL2_NO_SOUNDNESS_CHECKS
498 return check_term_UntypedIdentifierAssignment(t);
499#else
500 return true;
501#endif // MCRL2_NO_SOUNDNESS_CHECKS
502}
503
504template <atermpp::IsATerm Term>
505bool check_rule_DataSpec([[maybe_unused]] const Term& t)
506{
507#ifndef MCRL2_NO_SOUNDNESS_CHECKS
508 return check_term_DataSpec(t);
509#else
510 return true;
511#endif // MCRL2_NO_SOUNDNESS_CHECKS
512}
513
514template <atermpp::IsATerm Term>
515bool check_rule_SortSpec([[maybe_unused]] const Term& t)
516{
517#ifndef MCRL2_NO_SOUNDNESS_CHECKS
518 return check_term_SortSpec(t);
519#else
520 return true;
521#endif // MCRL2_NO_SOUNDNESS_CHECKS
522}
523
524template <atermpp::IsATerm Term>
525bool check_rule_ConsSpec([[maybe_unused]] const Term& t)
526{
527#ifndef MCRL2_NO_SOUNDNESS_CHECKS
528 return check_term_ConsSpec(t);
529#else
530 return true;
531#endif // MCRL2_NO_SOUNDNESS_CHECKS
532}
533
534template <atermpp::IsATerm Term>
535bool check_rule_MapSpec([[maybe_unused]] const Term& t)
536{
537#ifndef MCRL2_NO_SOUNDNESS_CHECKS
538 return check_term_MapSpec(t);
539#else
540 return true;
541#endif // MCRL2_NO_SOUNDNESS_CHECKS
542}
543
544template <atermpp::IsATerm Term>
546{
547#ifndef MCRL2_NO_SOUNDNESS_CHECKS
548 return check_term_DataEqnSpec(t);
549#else
550 return true;
551#endif // MCRL2_NO_SOUNDNESS_CHECKS
552}
553
554template <atermpp::IsATerm Term>
555bool check_rule_SortDecl([[maybe_unused]] const Term& t)
556{
557#ifndef MCRL2_NO_SOUNDNESS_CHECKS
558 return check_rule_SortId(t)
559 || check_term_SortRef(t);
560#else
561 return true;
562#endif // MCRL2_NO_SOUNDNESS_CHECKS
563}
564
565template <atermpp::IsATerm Term>
566bool check_rule_DataEqn([[maybe_unused]] const Term& t)
567{
568#ifndef MCRL2_NO_SOUNDNESS_CHECKS
569 return check_term_DataEqn(t);
570#else
571 return true;
572#endif // MCRL2_NO_SOUNDNESS_CHECKS
573}
574
575template <atermpp::IsATerm Term>
576bool check_rule_MultAct([[maybe_unused]] const Term& t)
577{
578#ifndef MCRL2_NO_SOUNDNESS_CHECKS
579 return check_term_MultAct(t);
580#else
581 return true;
582#endif // MCRL2_NO_SOUNDNESS_CHECKS
583}
584
585template <atermpp::IsATerm Term>
587{
588#ifndef MCRL2_NO_SOUNDNESS_CHECKS
589 return check_term_TimedMultAct(t);
590#else
591 return true;
592#endif // MCRL2_NO_SOUNDNESS_CHECKS
593}
594
595template <atermpp::IsATerm Term>
597{
598#ifndef MCRL2_NO_SOUNDNESS_CHECKS
599 return check_term_UntypedMultiAction(t);
600#else
601 return true;
602#endif // MCRL2_NO_SOUNDNESS_CHECKS
603}
604
605template <atermpp::IsATerm Term>
606bool check_rule_Action([[maybe_unused]] const Term& t)
607{
608#ifndef MCRL2_NO_SOUNDNESS_CHECKS
609 return check_term_Action(t);
610#else
611 return true;
612#endif // MCRL2_NO_SOUNDNESS_CHECKS
613}
614
615template <atermpp::IsATerm Term>
616bool check_rule_ActId([[maybe_unused]] const Term& t)
617{
618#ifndef MCRL2_NO_SOUNDNESS_CHECKS
619 return check_term_ActId(t);
620#else
621 return true;
622#endif // MCRL2_NO_SOUNDNESS_CHECKS
623}
624
625template <atermpp::IsATerm Term>
626bool check_rule_ProcExpr([[maybe_unused]] const Term& t)
627{
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)
633 || check_term_Tau(t)
634 || check_term_Sum(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)
642 || check_term_Seq(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);
652#else
653 return true;
654#endif // MCRL2_NO_SOUNDNESS_CHECKS
655}
656
657template <atermpp::IsATerm Term>
658bool check_rule_ProcVarId([[maybe_unused]] const Term& t)
659{
660#ifndef MCRL2_NO_SOUNDNESS_CHECKS
661 return check_term_ProcVarId(t);
662#else
663 return true;
664#endif // MCRL2_NO_SOUNDNESS_CHECKS
665}
666
667template <atermpp::IsATerm Term>
669{
670#ifndef MCRL2_NO_SOUNDNESS_CHECKS
671 return check_term_MultActName(t);
672#else
673 return true;
674#endif // MCRL2_NO_SOUNDNESS_CHECKS
675}
676
677template <atermpp::IsATerm Term>
678bool check_rule_RenameExpr([[maybe_unused]] const Term& t)
679{
680#ifndef MCRL2_NO_SOUNDNESS_CHECKS
681 return check_term_RenameExpr(t);
682#else
683 return true;
684#endif // MCRL2_NO_SOUNDNESS_CHECKS
685}
686
687template <atermpp::IsATerm Term>
688bool check_rule_CommExpr([[maybe_unused]] const Term& t)
689{
690#ifndef MCRL2_NO_SOUNDNESS_CHECKS
691 return check_term_CommExpr(t);
692#else
693 return true;
694#endif // MCRL2_NO_SOUNDNESS_CHECKS
695}
696
697template <atermpp::IsATerm Term>
698bool check_rule_ProcSpec([[maybe_unused]] const Term& t)
699{
700#ifndef MCRL2_NO_SOUNDNESS_CHECKS
701 return check_term_ProcSpec(t);
702#else
703 return true;
704#endif // MCRL2_NO_SOUNDNESS_CHECKS
705}
706
707template <atermpp::IsATerm Term>
708bool check_rule_ActSpec([[maybe_unused]] const Term& t)
709{
710#ifndef MCRL2_NO_SOUNDNESS_CHECKS
711 return check_term_ActSpec(t);
712#else
713 return true;
714#endif // MCRL2_NO_SOUNDNESS_CHECKS
715}
716
717template <atermpp::IsATerm Term>
719{
720#ifndef MCRL2_NO_SOUNDNESS_CHECKS
721 return check_term_GlobVarSpec(t);
722#else
723 return true;
724#endif // MCRL2_NO_SOUNDNESS_CHECKS
725}
726
727template <atermpp::IsATerm Term>
729{
730#ifndef MCRL2_NO_SOUNDNESS_CHECKS
731 return check_term_ProcEqnSpec(t);
732#else
733 return true;
734#endif // MCRL2_NO_SOUNDNESS_CHECKS
735}
736
737template <atermpp::IsATerm Term>
738bool check_rule_ProcEqn([[maybe_unused]] const Term& t)
739{
740#ifndef MCRL2_NO_SOUNDNESS_CHECKS
741 return check_term_ProcEqn(t);
742#else
743 return true;
744#endif // MCRL2_NO_SOUNDNESS_CHECKS
745}
746
747template <atermpp::IsATerm Term>
749{
750#ifndef MCRL2_NO_SOUNDNESS_CHECKS
751 return check_rule_MultAct(t)
752 || check_term_Delta(t);
753#else
754 return true;
755#endif // MCRL2_NO_SOUNDNESS_CHECKS
756}
757
758template <atermpp::IsATerm Term>
759bool check_rule_ProcInit([[maybe_unused]] const Term& t)
760{
761#ifndef MCRL2_NO_SOUNDNESS_CHECKS
762 return check_term_ProcessInit(t);
763#else
764 return true;
765#endif // MCRL2_NO_SOUNDNESS_CHECKS
766}
767
768template <atermpp::IsATerm Term>
770{
771#ifndef MCRL2_NO_SOUNDNESS_CHECKS
772 return check_term_Distribution(t);
773#else
774 return true;
775#endif // MCRL2_NO_SOUNDNESS_CHECKS
776}
777
778template <atermpp::IsATerm Term>
780{
781#ifndef MCRL2_NO_SOUNDNESS_CHECKS
782 return check_term_LinProcSpec(t);
783#else
784 return true;
785#endif // MCRL2_NO_SOUNDNESS_CHECKS
786}
787
788template <atermpp::IsATerm Term>
790{
791#ifndef MCRL2_NO_SOUNDNESS_CHECKS
792 return check_term_LinearProcess(t);
793#else
794 return true;
795#endif // MCRL2_NO_SOUNDNESS_CHECKS
796}
797
798template <atermpp::IsATerm Term>
800{
801#ifndef MCRL2_NO_SOUNDNESS_CHECKS
802 return check_term_LinearProcessSummand(t);
803#else
804 return true;
805#endif // MCRL2_NO_SOUNDNESS_CHECKS
806}
807
808template <atermpp::IsATerm Term>
810{
811#ifndef MCRL2_NO_SOUNDNESS_CHECKS
812 return check_term_LinearProcessInit(t);
813#else
814 return true;
815#endif // MCRL2_NO_SOUNDNESS_CHECKS
816}
817
818template <atermpp::IsATerm Term>
819bool check_rule_StateFrm([[maybe_unused]] const Term& t)
820{
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);
848#else
849 return true;
850#endif // MCRL2_NO_SOUNDNESS_CHECKS
851}
852
853template <atermpp::IsATerm Term>
854bool check_rule_RegFrm([[maybe_unused]] const Term& t)
855{
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);
864#else
865 return true;
866#endif // MCRL2_NO_SOUNDNESS_CHECKS
867}
868
869template <atermpp::IsATerm Term>
870bool check_rule_ActFrm([[maybe_unused]] const Term& t)
871{
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);
886#else
887 return true;
888#endif // MCRL2_NO_SOUNDNESS_CHECKS
889}
890
891template <atermpp::IsATerm Term>
893{
894#ifndef MCRL2_NO_SOUNDNESS_CHECKS
895 return check_rule_UntypedDataParameter(t)
896 || check_rule_Action(t);
897#else
898 return true;
899#endif // MCRL2_NO_SOUNDNESS_CHECKS
900}
901
902template <atermpp::IsATerm Term>
904{
905#ifndef MCRL2_NO_SOUNDNESS_CHECKS
906 return check_term_ActionRenameRules(t);
907#else
908 return true;
909#endif // MCRL2_NO_SOUNDNESS_CHECKS
910}
911
912template <atermpp::IsATerm Term>
914{
915#ifndef MCRL2_NO_SOUNDNESS_CHECKS
916 return check_term_ActionRenameRule(t);
917#else
918 return true;
919#endif // MCRL2_NO_SOUNDNESS_CHECKS
920}
921
922template <atermpp::IsATerm Term>
924{
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);
930#else
931 return true;
932#endif // MCRL2_NO_SOUNDNESS_CHECKS
933}
934
935template <atermpp::IsATerm Term>
937{
938#ifndef MCRL2_NO_SOUNDNESS_CHECKS
939 return check_term_ActionRenameSpec(t);
940#else
941 return true;
942#endif // MCRL2_NO_SOUNDNESS_CHECKS
943}
944
945template <atermpp::IsATerm Term>
946bool check_rule_PBES([[maybe_unused]] const Term& t)
947{
948#ifndef MCRL2_NO_SOUNDNESS_CHECKS
949 return check_term_PBES(t);
950#else
951 return true;
952#endif // MCRL2_NO_SOUNDNESS_CHECKS
953}
954
955template <atermpp::IsATerm Term>
956bool check_rule_PBEqnSpec([[maybe_unused]] const Term& t)
957{
958#ifndef MCRL2_NO_SOUNDNESS_CHECKS
959 return check_term_PBEqnSpec(t);
960#else
961 return true;
962#endif // MCRL2_NO_SOUNDNESS_CHECKS
963}
964
965template <atermpp::IsATerm Term>
966bool check_rule_PBInit([[maybe_unused]] const Term& t)
967{
968#ifndef MCRL2_NO_SOUNDNESS_CHECKS
969 return check_term_PBInit(t);
970#else
971 return true;
972#endif // MCRL2_NO_SOUNDNESS_CHECKS
973}
974
975template <atermpp::IsATerm Term>
976bool check_rule_PBEqn([[maybe_unused]] const Term& t)
977{
978#ifndef MCRL2_NO_SOUNDNESS_CHECKS
979 return check_term_PBEqn(t);
980#else
981 return true;
982#endif // MCRL2_NO_SOUNDNESS_CHECKS
983}
984
985template <atermpp::IsATerm Term>
986bool check_rule_FixPoint([[maybe_unused]] const Term& t)
987{
988#ifndef MCRL2_NO_SOUNDNESS_CHECKS
989 return check_term_Mu(t)
990 || check_term_Nu(t);
991#else
992 return true;
993#endif // MCRL2_NO_SOUNDNESS_CHECKS
994}
995
996template <atermpp::IsATerm Term>
998{
999#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1000 return check_term_PropVarDecl(t);
1001#else
1002 return true;
1003#endif // MCRL2_NO_SOUNDNESS_CHECKS
1004}
1005
1006template <atermpp::IsATerm Term>
1007bool check_rule_PBExpr([[maybe_unused]] const Term& t)
1008{
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);
1021#else
1022 return true;
1023#endif // MCRL2_NO_SOUNDNESS_CHECKS
1024}
1025
1026template <atermpp::IsATerm Term>
1028{
1029#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1030 return check_term_PropVarInst(t);
1031#else
1032 return true;
1033#endif // MCRL2_NO_SOUNDNESS_CHECKS
1034}
1035
1036template <atermpp::IsATerm Term>
1037bool check_rule_PRES([[maybe_unused]] const Term& t)
1038{
1039#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1040 return check_term_PRES(t);
1041#else
1042 return true;
1043#endif // MCRL2_NO_SOUNDNESS_CHECKS
1044}
1045
1046template <atermpp::IsATerm Term>
1047bool check_rule_PREqnSpec([[maybe_unused]] const Term& t)
1048{
1049#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1050 return check_term_PREqnSpec(t);
1051#else
1052 return true;
1053#endif // MCRL2_NO_SOUNDNESS_CHECKS
1054}
1055
1056template <atermpp::IsATerm Term>
1057bool check_rule_PRInit([[maybe_unused]] const Term& t)
1058{
1059#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1060 return check_term_PRInit(t);
1061#else
1062 return true;
1063#endif // MCRL2_NO_SOUNDNESS_CHECKS
1064}
1065
1066template <atermpp::IsATerm Term>
1067bool check_rule_PREqn([[maybe_unused]] const Term& t)
1068{
1069#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1070 return check_term_PREqn(t);
1071#else
1072 return true;
1073#endif // MCRL2_NO_SOUNDNESS_CHECKS
1074}
1075
1076template <atermpp::IsATerm Term>
1077bool check_rule_PRExpr([[maybe_unused]] const Term& t)
1078{
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);
1099#else
1100 return true;
1101#endif // MCRL2_NO_SOUNDNESS_CHECKS
1102}
1103
1104// SortCons(SortConsType, SortExpr)
1105template <atermpp::IsATerm Term>
1106bool check_term_SortCons([[maybe_unused]] const Term& t)
1107{
1108#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1109 // check the type of the term
1110 const atermpp::aterm& term(t);
1111 if (!term.type_is_appl())
1112 {
1113 return false;
1114 }
1115 if (term.function() != core::detail::function_symbols::SortCons)
1116 {
1117 return false;
1118 }
1119
1120 // check the children
1121 if (term.size() != 2)
1122 {
1123 return false;
1124 }
1125#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1126 if (!check_term_argument(term[0], check_rule_SortConsType<atermpp::aterm>))
1127 {
1128 mCRL2log(log::log_level_t::debug) << "check_rule_SortConsType" << std::endl;
1129 return false;
1130 }
1131 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1132 {
1133 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
1134 return false;
1135 }
1136#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1137
1138#endif // MCRL2_NO_SOUNDNESS_CHECKS
1139 return true;
1140}
1141
1142// SortStruct(StructCons+)
1143template <atermpp::IsATerm Term>
1145{
1146#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1147 // check the type of the term
1148 const atermpp::aterm& term(t);
1149 if (!term.type_is_appl())
1150 {
1151 return false;
1152 }
1153 if (term.function() != core::detail::function_symbols::SortStruct)
1154 {
1155 return false;
1156 }
1157
1158 // check the children
1159 if (term.size() != 1)
1160 {
1161 return false;
1162 }
1163#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1164 if (!check_list_argument(term[0], check_rule_StructCons<atermpp::aterm>, 1))
1165 {
1166 mCRL2log(log::log_level_t::debug) << "check_rule_StructCons" << std::endl;
1167 return false;
1168 }
1169#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1170
1171#endif // MCRL2_NO_SOUNDNESS_CHECKS
1172 return true;
1173}
1174
1175// SortArrow(SortExpr+, SortExpr)
1176template <atermpp::IsATerm Term>
1177bool check_term_SortArrow([[maybe_unused]] const Term& t)
1178{
1179#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1180 // check the type of the term
1181 const atermpp::aterm& term(t);
1182 if (!term.type_is_appl())
1183 {
1184 return false;
1185 }
1186 if (term.function() != core::detail::function_symbols::SortArrow)
1187 {
1188 return false;
1189 }
1190
1191 // check the children
1192 if (term.size() != 2)
1193 {
1194 return false;
1195 }
1196#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1197 if (!check_list_argument(term[0], check_rule_SortExpr<atermpp::aterm>, 1))
1198 {
1199 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
1200 return false;
1201 }
1202 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1203 {
1204 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
1205 return false;
1206 }
1207#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1208
1209#endif // MCRL2_NO_SOUNDNESS_CHECKS
1210 return true;
1211}
1212
1213// UntypedSortUnknown()
1214template <atermpp::IsATerm Term>
1216{
1217#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1218 // check the type of the term
1219 const atermpp::aterm& term(t);
1220 if (!term.type_is_appl())
1221 {
1222 return false;
1223 }
1224 if (term.function() != core::detail::function_symbols::UntypedSortUnknown)
1225 {
1226 return false;
1227 }
1228
1229 // check the children
1230 if (term.size() != 0)
1231 {
1232 return false;
1233 }
1234
1235#endif // MCRL2_NO_SOUNDNESS_CHECKS
1236 return true;
1237}
1238
1239// UntypedSortsPossible(SortExpr+)
1240template <atermpp::IsATerm Term>
1242{
1243#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1244 // check the type of the term
1245 const atermpp::aterm& term(t);
1246 if (!term.type_is_appl())
1247 {
1248 return false;
1249 }
1250 if (term.function() != core::detail::function_symbols::UntypedSortsPossible)
1251 {
1252 return false;
1253 }
1254
1255 // check the children
1256 if (term.size() != 1)
1257 {
1258 return false;
1259 }
1260#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1261 if (!check_list_argument(term[0], check_rule_SortExpr<atermpp::aterm>, 1))
1262 {
1263 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
1264 return false;
1265 }
1266#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1267
1268#endif // MCRL2_NO_SOUNDNESS_CHECKS
1269 return true;
1270}
1271
1272// UntypedSortVariable(Number)
1273template <atermpp::IsATerm Term>
1275{
1276#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1277 // check the type of the term
1278 const atermpp::aterm& term(t);
1279 if (!term.type_is_appl())
1280 {
1281 return false;
1282 }
1283 if (term.function() != core::detail::function_symbols::UntypedSortVariable)
1284 {
1285 return false;
1286 }
1287
1288 // check the children
1289 if (term.size() != 1)
1290 {
1291 return false;
1292 }
1293#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1294 if (!check_term_argument(term[0], check_rule_Number<atermpp::aterm>))
1295 {
1296 mCRL2log(log::log_level_t::debug) << "check_rule_Number" << std::endl;
1297 return false;
1298 }
1299#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1300
1301#endif // MCRL2_NO_SOUNDNESS_CHECKS
1302 return true;
1303}
1304
1305// SortId(String)
1306template <atermpp::IsATerm Term>
1307bool check_term_SortId([[maybe_unused]] const Term& t)
1308{
1309#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1310 // check the type of the term
1311 const atermpp::aterm& term(t);
1312 if (!term.type_is_appl())
1313 {
1314 return false;
1315 }
1316 if (term.function() != core::detail::function_symbols::SortId)
1317 {
1318 return false;
1319 }
1320
1321 // check the children
1322 if (term.size() != 1)
1323 {
1324 return false;
1325 }
1326#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1327 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1328 {
1329 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
1330 return false;
1331 }
1332#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1333
1334#endif // MCRL2_NO_SOUNDNESS_CHECKS
1335 return true;
1336}
1337
1338// SortList()
1339template <atermpp::IsATerm Term>
1340bool check_term_SortList([[maybe_unused]] const Term& t)
1341{
1342#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1343 // check the type of the term
1344 const atermpp::aterm& term(t);
1345 if (!term.type_is_appl())
1346 {
1347 return false;
1348 }
1349 if (term.function() != core::detail::function_symbols::SortList)
1350 {
1351 return false;
1352 }
1353
1354 // check the children
1355 if (term.size() != 0)
1356 {
1357 return false;
1358 }
1359
1360#endif // MCRL2_NO_SOUNDNESS_CHECKS
1361 return true;
1362}
1363
1364// SortSet()
1365template <atermpp::IsATerm Term>
1366bool check_term_SortSet([[maybe_unused]] const Term& t)
1367{
1368#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1369 // check the type of the term
1370 const atermpp::aterm& term(t);
1371 if (!term.type_is_appl())
1372 {
1373 return false;
1374 }
1375 if (term.function() != core::detail::function_symbols::SortSet)
1376 {
1377 return false;
1378 }
1379
1380 // check the children
1381 if (term.size() != 0)
1382 {
1383 return false;
1384 }
1385
1386#endif // MCRL2_NO_SOUNDNESS_CHECKS
1387 return true;
1388}
1389
1390// SortBag()
1391template <atermpp::IsATerm Term>
1392bool check_term_SortBag([[maybe_unused]] const Term& t)
1393{
1394#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1395 // check the type of the term
1396 const atermpp::aterm& term(t);
1397 if (!term.type_is_appl())
1398 {
1399 return false;
1400 }
1401 if (term.function() != core::detail::function_symbols::SortBag)
1402 {
1403 return false;
1404 }
1405
1406 // check the children
1407 if (term.size() != 0)
1408 {
1409 return false;
1410 }
1411
1412#endif // MCRL2_NO_SOUNDNESS_CHECKS
1413 return true;
1414}
1415
1416// SortFSet()
1417template <atermpp::IsATerm Term>
1418bool check_term_SortFSet([[maybe_unused]] const Term& t)
1419{
1420#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1421 // check the type of the term
1422 const atermpp::aterm& term(t);
1423 if (!term.type_is_appl())
1424 {
1425 return false;
1426 }
1427 if (term.function() != core::detail::function_symbols::SortFSet)
1428 {
1429 return false;
1430 }
1431
1432 // check the children
1433 if (term.size() != 0)
1434 {
1435 return false;
1436 }
1437
1438#endif // MCRL2_NO_SOUNDNESS_CHECKS
1439 return true;
1440}
1441
1442// SortFBag()
1443template <atermpp::IsATerm Term>
1444bool check_term_SortFBag([[maybe_unused]] const Term& t)
1445{
1446#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1447 // check the type of the term
1448 const atermpp::aterm& term(t);
1449 if (!term.type_is_appl())
1450 {
1451 return false;
1452 }
1453 if (term.function() != core::detail::function_symbols::SortFBag)
1454 {
1455 return false;
1456 }
1457
1458 // check the children
1459 if (term.size() != 0)
1460 {
1461 return false;
1462 }
1463
1464#endif // MCRL2_NO_SOUNDNESS_CHECKS
1465 return true;
1466}
1467
1468// StructCons(String, StructProj*, StringOrEmpty)
1469template <atermpp::IsATerm Term>
1471{
1472#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1473 // check the type of the term
1474 const atermpp::aterm& term(t);
1475 if (!term.type_is_appl())
1476 {
1477 return false;
1478 }
1479 if (term.function() != core::detail::function_symbols::StructCons)
1480 {
1481 return false;
1482 }
1483
1484 // check the children
1485 if (term.size() != 3)
1486 {
1487 return false;
1488 }
1489#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1490 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1491 {
1492 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
1493 return false;
1494 }
1495 if (!check_list_argument(term[1], check_rule_StructProj<atermpp::aterm>, 0))
1496 {
1497 mCRL2log(log::log_level_t::debug) << "check_rule_StructProj" << std::endl;
1498 return false;
1499 }
1500 if (!check_term_argument(term[2], check_rule_StringOrEmpty<atermpp::aterm>))
1501 {
1502 mCRL2log(log::log_level_t::debug) << "check_rule_StringOrEmpty" << std::endl;
1503 return false;
1504 }
1505#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1506
1507#endif // MCRL2_NO_SOUNDNESS_CHECKS
1508 return true;
1509}
1510
1511// StructProj(StringOrEmpty, SortExpr)
1512template <atermpp::IsATerm Term>
1514{
1515#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1516 // check the type of the term
1517 const atermpp::aterm& term(t);
1518 if (!term.type_is_appl())
1519 {
1520 return false;
1521 }
1522 if (term.function() != core::detail::function_symbols::StructProj)
1523 {
1524 return false;
1525 }
1526
1527 // check the children
1528 if (term.size() != 2)
1529 {
1530 return false;
1531 }
1532#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1533 if (!check_term_argument(term[0], check_rule_StringOrEmpty<atermpp::aterm>))
1534 {
1535 mCRL2log(log::log_level_t::debug) << "check_rule_StringOrEmpty" << std::endl;
1536 return false;
1537 }
1538 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1539 {
1540 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
1541 return false;
1542 }
1543#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1544
1545#endif // MCRL2_NO_SOUNDNESS_CHECKS
1546 return true;
1547}
1548
1549// Binder(BindingOperator, DataVarId+, DataExpr)
1550template <atermpp::IsATerm Term>
1551bool check_term_Binder([[maybe_unused]] const Term& t)
1552{
1553#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1554 // check the type of the term
1555 const atermpp::aterm& term(t);
1556 if (!term.type_is_appl())
1557 {
1558 return false;
1559 }
1560 if (term.function() != core::detail::function_symbols::Binder)
1561 {
1562 return false;
1563 }
1564
1565 // check the children
1566 if (term.size() != 3)
1567 {
1568 return false;
1569 }
1570#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1571 if (!check_term_argument(term[0], check_rule_BindingOperator<atermpp::aterm>))
1572 {
1573 mCRL2log(log::log_level_t::debug) << "check_rule_BindingOperator" << std::endl;
1574 return false;
1575 }
1576 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 1))
1577 {
1578 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
1579 return false;
1580 }
1581 if (!check_term_argument(term[2], check_rule_DataExpr<atermpp::aterm>))
1582 {
1583 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
1584 return false;
1585 }
1586#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1587
1588#endif // MCRL2_NO_SOUNDNESS_CHECKS
1589 return true;
1590}
1591
1592// Whr(DataExpr, WhrDecl+)
1593template <atermpp::IsATerm Term>
1594bool check_term_Whr([[maybe_unused]] const Term& t)
1595{
1596#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1597 // check the type of the term
1598 const atermpp::aterm& term(t);
1599 if (!term.type_is_appl())
1600 {
1601 return false;
1602 }
1603 if (term.function() != core::detail::function_symbols::Whr)
1604 {
1605 return false;
1606 }
1607
1608 // check the children
1609 if (term.size() != 2)
1610 {
1611 return false;
1612 }
1613#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1614 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
1615 {
1616 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
1617 return false;
1618 }
1619 if (!check_list_argument(term[1], check_rule_WhrDecl<atermpp::aterm>, 1))
1620 {
1621 mCRL2log(log::log_level_t::debug) << "check_rule_WhrDecl" << std::endl;
1622 return false;
1623 }
1624#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1625
1626#endif // MCRL2_NO_SOUNDNESS_CHECKS
1627 return true;
1628}
1629
1630// UntypedIdentifier(String)
1631template <atermpp::IsATerm Term>
1633{
1634#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1635 // check the type of the term
1636 const atermpp::aterm& term(t);
1637 if (!term.type_is_appl())
1638 {
1639 return false;
1640 }
1641 if (term.function() != core::detail::function_symbols::UntypedIdentifier)
1642 {
1643 return false;
1644 }
1645
1646 // check the children
1647 if (term.size() != 1)
1648 {
1649 return false;
1650 }
1651#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1652 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1653 {
1654 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
1655 return false;
1656 }
1657#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1658
1659#endif // MCRL2_NO_SOUNDNESS_CHECKS
1660 return true;
1661}
1662
1663// DataVarId(String, SortExpr)
1664template <atermpp::IsATerm Term>
1665bool check_term_DataVarId([[maybe_unused]] const Term& t)
1666{
1667#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1668 // check the type of the term
1669 const atermpp::aterm& term(t);
1670 if (!term.type_is_appl())
1671 {
1672 return false;
1673 }
1674 if (term.function() != core::detail::function_symbols::DataVarId)
1675 {
1676 return false;
1677 }
1678
1679 // check the children
1680 if (term.size() != 2)
1681 {
1682 return false;
1683 }
1684#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1685 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1686 {
1687 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
1688 return false;
1689 }
1690 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1691 {
1692 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
1693 return false;
1694 }
1695#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1696
1697#endif // MCRL2_NO_SOUNDNESS_CHECKS
1698 return true;
1699}
1700
1701// OpId(String, SortExpr, Number)
1702template <atermpp::IsATerm Term>
1703bool check_term_OpId([[maybe_unused]] const Term& t)
1704{
1705#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1706 // check the type of the term
1707 const atermpp::aterm& term(t);
1708 if (!term.type_is_appl())
1709 {
1710 return false;
1711 }
1712 if (term.function() != core::detail::function_symbols::OpId)
1713 {
1714 return false;
1715 }
1716
1717 // check the children
1718 if (term.size() != 3)
1719 {
1720 return false;
1721 }
1722#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1723 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1724 {
1725 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
1726 return false;
1727 }
1728 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1729 {
1730 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
1731 return false;
1732 }
1733 if (!check_term_argument(term[2], check_rule_Number<atermpp::aterm>))
1734 {
1735 mCRL2log(log::log_level_t::debug) << "check_rule_Number" << std::endl;
1736 return false;
1737 }
1738#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1739
1740#endif // MCRL2_NO_SOUNDNESS_CHECKS
1741 return true;
1742}
1743
1744// UntypedDataParameter(String, DataExpr*)
1745template <atermpp::IsATerm Term>
1747{
1748#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1749 // check the type of the term
1750 const atermpp::aterm& term(t);
1751 if (!term.type_is_appl())
1752 {
1753 return false;
1754 }
1755 if (term.function() != core::detail::function_symbols::UntypedDataParameter)
1756 {
1757 return false;
1758 }
1759
1760 // check the children
1761 if (term.size() != 2)
1762 {
1763 return false;
1764 }
1765#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1766 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1767 {
1768 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
1769 return false;
1770 }
1771 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
1772 {
1773 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
1774 return false;
1775 }
1776#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1777
1778#endif // MCRL2_NO_SOUNDNESS_CHECKS
1779 return true;
1780}
1781
1782// Forall()
1783template <atermpp::IsATerm Term>
1784bool check_term_Forall([[maybe_unused]] const Term& t)
1785{
1786#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1787 // check the type of the term
1788 const atermpp::aterm& term(t);
1789 if (!term.type_is_appl())
1790 {
1791 return false;
1792 }
1793 if (term.function() != core::detail::function_symbols::Forall)
1794 {
1795 return false;
1796 }
1797
1798 // check the children
1799 if (term.size() != 0)
1800 {
1801 return false;
1802 }
1803
1804#endif // MCRL2_NO_SOUNDNESS_CHECKS
1805 return true;
1806}
1807
1808// Exists()
1809template <atermpp::IsATerm Term>
1810bool check_term_Exists([[maybe_unused]] const Term& t)
1811{
1812#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1813 // check the type of the term
1814 const atermpp::aterm& term(t);
1815 if (!term.type_is_appl())
1816 {
1817 return false;
1818 }
1819 if (term.function() != core::detail::function_symbols::Exists)
1820 {
1821 return false;
1822 }
1823
1824 // check the children
1825 if (term.size() != 0)
1826 {
1827 return false;
1828 }
1829
1830#endif // MCRL2_NO_SOUNDNESS_CHECKS
1831 return true;
1832}
1833
1834// SetComp()
1835template <atermpp::IsATerm Term>
1836bool check_term_SetComp([[maybe_unused]] const Term& t)
1837{
1838#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1839 // check the type of the term
1840 const atermpp::aterm& term(t);
1841 if (!term.type_is_appl())
1842 {
1843 return false;
1844 }
1845 if (term.function() != core::detail::function_symbols::SetComp)
1846 {
1847 return false;
1848 }
1849
1850 // check the children
1851 if (term.size() != 0)
1852 {
1853 return false;
1854 }
1855
1856#endif // MCRL2_NO_SOUNDNESS_CHECKS
1857 return true;
1858}
1859
1860// BagComp()
1861template <atermpp::IsATerm Term>
1862bool check_term_BagComp([[maybe_unused]] const Term& t)
1863{
1864#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1865 // check the type of the term
1866 const atermpp::aterm& term(t);
1867 if (!term.type_is_appl())
1868 {
1869 return false;
1870 }
1871 if (term.function() != core::detail::function_symbols::BagComp)
1872 {
1873 return false;
1874 }
1875
1876 // check the children
1877 if (term.size() != 0)
1878 {
1879 return false;
1880 }
1881
1882#endif // MCRL2_NO_SOUNDNESS_CHECKS
1883 return true;
1884}
1885
1886// Lambda()
1887template <atermpp::IsATerm Term>
1888bool check_term_Lambda([[maybe_unused]] const Term& t)
1889{
1890#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1891 // check the type of the term
1892 const atermpp::aterm& term(t);
1893 if (!term.type_is_appl())
1894 {
1895 return false;
1896 }
1897 if (term.function() != core::detail::function_symbols::Lambda)
1898 {
1899 return false;
1900 }
1901
1902 // check the children
1903 if (term.size() != 0)
1904 {
1905 return false;
1906 }
1907
1908#endif // MCRL2_NO_SOUNDNESS_CHECKS
1909 return true;
1910}
1911
1912// UntypedSetBagComp()
1913template <atermpp::IsATerm Term>
1915{
1916#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1917 // check the type of the term
1918 const atermpp::aterm& term(t);
1919 if (!term.type_is_appl())
1920 {
1921 return false;
1922 }
1923 if (term.function() != core::detail::function_symbols::UntypedSetBagComp)
1924 {
1925 return false;
1926 }
1927
1928 // check the children
1929 if (term.size() != 0)
1930 {
1931 return false;
1932 }
1933
1934#endif // MCRL2_NO_SOUNDNESS_CHECKS
1935 return true;
1936}
1937
1938// DataVarIdInit(DataVarId, DataExpr)
1939template <atermpp::IsATerm Term>
1941{
1942#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1943 // check the type of the term
1944 const atermpp::aterm& term(t);
1945 if (!term.type_is_appl())
1946 {
1947 return false;
1948 }
1949 if (term.function() != core::detail::function_symbols::DataVarIdInit)
1950 {
1951 return false;
1952 }
1953
1954 // check the children
1955 if (term.size() != 2)
1956 {
1957 return false;
1958 }
1959#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1960 if (!check_term_argument(term[0], check_rule_DataVarId<atermpp::aterm>))
1961 {
1962 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
1963 return false;
1964 }
1965 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
1966 {
1967 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
1968 return false;
1969 }
1970#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1971
1972#endif // MCRL2_NO_SOUNDNESS_CHECKS
1973 return true;
1974}
1975
1976// UntypedIdentifierAssignment(String, DataExpr)
1977template <atermpp::IsATerm Term>
1979{
1980#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1981 // check the type of the term
1982 const atermpp::aterm& term(t);
1983 if (!term.type_is_appl())
1984 {
1985 return false;
1986 }
1987 if (term.function() != core::detail::function_symbols::UntypedIdentifierAssignment)
1988 {
1989 return false;
1990 }
1991
1992 // check the children
1993 if (term.size() != 2)
1994 {
1995 return false;
1996 }
1997#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1998 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1999 {
2000 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
2001 return false;
2002 }
2003 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2004 {
2005 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2006 return false;
2007 }
2008#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2009
2010#endif // MCRL2_NO_SOUNDNESS_CHECKS
2011 return true;
2012}
2013
2014// DataSpec(SortSpec, ConsSpec, MapSpec, DataEqnSpec)
2015template <atermpp::IsATerm Term>
2016bool check_term_DataSpec([[maybe_unused]] const Term& t)
2017{
2018#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2019 // check the type of the term
2020 const atermpp::aterm& term(t);
2021 if (!term.type_is_appl())
2022 {
2023 return false;
2024 }
2025 if (term.function() != core::detail::function_symbols::DataSpec)
2026 {
2027 return false;
2028 }
2029
2030 // check the children
2031 if (term.size() != 4)
2032 {
2033 return false;
2034 }
2035#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2036 if (!check_term_argument(term[0], check_rule_SortSpec<atermpp::aterm>))
2037 {
2038 mCRL2log(log::log_level_t::debug) << "check_rule_SortSpec" << std::endl;
2039 return false;
2040 }
2041 if (!check_term_argument(term[1], check_rule_ConsSpec<atermpp::aterm>))
2042 {
2043 mCRL2log(log::log_level_t::debug) << "check_rule_ConsSpec" << std::endl;
2044 return false;
2045 }
2046 if (!check_term_argument(term[2], check_rule_MapSpec<atermpp::aterm>))
2047 {
2048 mCRL2log(log::log_level_t::debug) << "check_rule_MapSpec" << std::endl;
2049 return false;
2050 }
2051 if (!check_term_argument(term[3], check_rule_DataEqnSpec<atermpp::aterm>))
2052 {
2053 mCRL2log(log::log_level_t::debug) << "check_rule_DataEqnSpec" << std::endl;
2054 return false;
2055 }
2056#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2057
2058#endif // MCRL2_NO_SOUNDNESS_CHECKS
2059 return true;
2060}
2061
2062// SortSpec(SortDecl*)
2063template <atermpp::IsATerm Term>
2064bool check_term_SortSpec([[maybe_unused]] const Term& t)
2065{
2066#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2067 // check the type of the term
2068 const atermpp::aterm& term(t);
2069 if (!term.type_is_appl())
2070 {
2071 return false;
2072 }
2073 if (term.function() != core::detail::function_symbols::SortSpec)
2074 {
2075 return false;
2076 }
2077
2078 // check the children
2079 if (term.size() != 1)
2080 {
2081 return false;
2082 }
2083#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2084 if (!check_list_argument(term[0], check_rule_SortDecl<atermpp::aterm>, 0))
2085 {
2086 mCRL2log(log::log_level_t::debug) << "check_rule_SortDecl" << std::endl;
2087 return false;
2088 }
2089#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2090
2091#endif // MCRL2_NO_SOUNDNESS_CHECKS
2092 return true;
2093}
2094
2095// ConsSpec(OpId*)
2096template <atermpp::IsATerm Term>
2097bool check_term_ConsSpec([[maybe_unused]] const Term& t)
2098{
2099#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2100 // check the type of the term
2101 const atermpp::aterm& term(t);
2102 if (!term.type_is_appl())
2103 {
2104 return false;
2105 }
2106 if (term.function() != core::detail::function_symbols::ConsSpec)
2107 {
2108 return false;
2109 }
2110
2111 // check the children
2112 if (term.size() != 1)
2113 {
2114 return false;
2115 }
2116#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2117 if (!check_list_argument(term[0], check_rule_OpId<atermpp::aterm>, 0))
2118 {
2119 mCRL2log(log::log_level_t::debug) << "check_rule_OpId" << std::endl;
2120 return false;
2121 }
2122#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2123
2124#endif // MCRL2_NO_SOUNDNESS_CHECKS
2125 return true;
2126}
2127
2128// MapSpec(OpId*)
2129template <atermpp::IsATerm Term>
2130bool check_term_MapSpec([[maybe_unused]] const Term& t)
2131{
2132#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2133 // check the type of the term
2134 const atermpp::aterm& term(t);
2135 if (!term.type_is_appl())
2136 {
2137 return false;
2138 }
2139 if (term.function() != core::detail::function_symbols::MapSpec)
2140 {
2141 return false;
2142 }
2143
2144 // check the children
2145 if (term.size() != 1)
2146 {
2147 return false;
2148 }
2149#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2150 if (!check_list_argument(term[0], check_rule_OpId<atermpp::aterm>, 0))
2151 {
2152 mCRL2log(log::log_level_t::debug) << "check_rule_OpId" << std::endl;
2153 return false;
2154 }
2155#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2156
2157#endif // MCRL2_NO_SOUNDNESS_CHECKS
2158 return true;
2159}
2160
2161// DataEqnSpec(DataEqn*)
2162template <atermpp::IsATerm Term>
2164{
2165#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2166 // check the type of the term
2167 const atermpp::aterm& term(t);
2168 if (!term.type_is_appl())
2169 {
2170 return false;
2171 }
2172 if (term.function() != core::detail::function_symbols::DataEqnSpec)
2173 {
2174 return false;
2175 }
2176
2177 // check the children
2178 if (term.size() != 1)
2179 {
2180 return false;
2181 }
2182#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2183 if (!check_list_argument(term[0], check_rule_DataEqn<atermpp::aterm>, 0))
2184 {
2185 mCRL2log(log::log_level_t::debug) << "check_rule_DataEqn" << std::endl;
2186 return false;
2187 }
2188#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2189
2190#endif // MCRL2_NO_SOUNDNESS_CHECKS
2191 return true;
2192}
2193
2194// SortRef(SortId, SortExpr)
2195template <atermpp::IsATerm Term>
2196bool check_term_SortRef([[maybe_unused]] const Term& t)
2197{
2198#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2199 // check the type of the term
2200 const atermpp::aterm& term(t);
2201 if (!term.type_is_appl())
2202 {
2203 return false;
2204 }
2205 if (term.function() != core::detail::function_symbols::SortRef)
2206 {
2207 return false;
2208 }
2209
2210 // check the children
2211 if (term.size() != 2)
2212 {
2213 return false;
2214 }
2215#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2216 if (!check_term_argument(term[0], check_rule_SortId<atermpp::aterm>))
2217 {
2218 mCRL2log(log::log_level_t::debug) << "check_rule_SortId" << std::endl;
2219 return false;
2220 }
2221 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
2222 {
2223 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
2224 return false;
2225 }
2226#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2227
2228#endif // MCRL2_NO_SOUNDNESS_CHECKS
2229 return true;
2230}
2231
2232// DataEqn(DataVarId*, DataExpr, DataExpr, DataExpr)
2233template <atermpp::IsATerm Term>
2234bool check_term_DataEqn([[maybe_unused]] const Term& t)
2235{
2236#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2237 // check the type of the term
2238 const atermpp::aterm& term(t);
2239 if (!term.type_is_appl())
2240 {
2241 return false;
2242 }
2243 if (term.function() != core::detail::function_symbols::DataEqn)
2244 {
2245 return false;
2246 }
2247
2248 // check the children
2249 if (term.size() != 4)
2250 {
2251 return false;
2252 }
2253#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2254 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
2255 {
2256 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
2257 return false;
2258 }
2259 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2260 {
2261 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2262 return false;
2263 }
2264 if (!check_term_argument(term[2], check_rule_DataExpr<atermpp::aterm>))
2265 {
2266 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2267 return false;
2268 }
2269 if (!check_term_argument(term[3], check_rule_DataExpr<atermpp::aterm>))
2270 {
2271 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2272 return false;
2273 }
2274#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2275
2276#endif // MCRL2_NO_SOUNDNESS_CHECKS
2277 return true;
2278}
2279
2280// MultAct(Action*)
2281template <atermpp::IsATerm Term>
2282bool check_term_MultAct([[maybe_unused]] const Term& t)
2283{
2284#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2285 // check the type of the term
2286 const atermpp::aterm& term(t);
2287 if (!term.type_is_appl())
2288 {
2289 return false;
2290 }
2291 if (term.function() != core::detail::function_symbols::MultAct)
2292 {
2293 return false;
2294 }
2295
2296 // check the children
2297 if (term.size() != 1)
2298 {
2299 return false;
2300 }
2301#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2302 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
2303 {
2304 mCRL2log(log::log_level_t::debug) << "check_rule_Action" << std::endl;
2305 return false;
2306 }
2307#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2308
2309#endif // MCRL2_NO_SOUNDNESS_CHECKS
2310 return true;
2311}
2312
2313// TimedMultAct(Action*, DataExpr)
2314template <atermpp::IsATerm Term>
2316{
2317#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2318 // check the type of the term
2319 const atermpp::aterm& term(t);
2320 if (!term.type_is_appl())
2321 {
2322 return false;
2323 }
2324 if (term.function() != core::detail::function_symbols::TimedMultAct)
2325 {
2326 return false;
2327 }
2328
2329 // check the children
2330 if (term.size() != 2)
2331 {
2332 return false;
2333 }
2334#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2335 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
2336 {
2337 mCRL2log(log::log_level_t::debug) << "check_rule_Action" << std::endl;
2338 return false;
2339 }
2340 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2341 {
2342 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2343 return false;
2344 }
2345#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2346
2347#endif // MCRL2_NO_SOUNDNESS_CHECKS
2348 return true;
2349}
2350
2351// UntypedMultiAction(UntypedDataParameter*)
2352template <atermpp::IsATerm Term>
2354{
2355#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2356 // check the type of the term
2357 const atermpp::aterm& term(t);
2358 if (!term.type_is_appl())
2359 {
2360 return false;
2361 }
2362 if (term.function() != core::detail::function_symbols::UntypedMultiAction)
2363 {
2364 return false;
2365 }
2366
2367 // check the children
2368 if (term.size() != 1)
2369 {
2370 return false;
2371 }
2372#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2373 if (!check_list_argument(term[0], check_rule_UntypedDataParameter<atermpp::aterm>, 0))
2374 {
2375 mCRL2log(log::log_level_t::debug) << "check_rule_UntypedDataParameter" << std::endl;
2376 return false;
2377 }
2378#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2379
2380#endif // MCRL2_NO_SOUNDNESS_CHECKS
2381 return true;
2382}
2383
2384// Action(ActId, DataExpr*)
2385template <atermpp::IsATerm Term>
2386bool check_term_Action([[maybe_unused]] const Term& t)
2387{
2388#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2389 // check the type of the term
2390 const atermpp::aterm& term(t);
2391 if (!term.type_is_appl())
2392 {
2393 return false;
2394 }
2395 if (term.function() != core::detail::function_symbols::Action)
2396 {
2397 return false;
2398 }
2399
2400 // check the children
2401 if (term.size() != 2)
2402 {
2403 return false;
2404 }
2405#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2406 if (!check_term_argument(term[0], check_rule_ActId<atermpp::aterm>))
2407 {
2408 mCRL2log(log::log_level_t::debug) << "check_rule_ActId" << std::endl;
2409 return false;
2410 }
2411 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
2412 {
2413 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2414 return false;
2415 }
2416#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2417
2418#endif // MCRL2_NO_SOUNDNESS_CHECKS
2419 return true;
2420}
2421
2422// ActId(String, SortExpr*)
2423template <atermpp::IsATerm Term>
2424bool check_term_ActId([[maybe_unused]] const Term& t)
2425{
2426#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2427 // check the type of the term
2428 const atermpp::aterm& term(t);
2429 if (!term.type_is_appl())
2430 {
2431 return false;
2432 }
2433 if (term.function() != core::detail::function_symbols::ActId)
2434 {
2435 return false;
2436 }
2437
2438 // check the children
2439 if (term.size() != 2)
2440 {
2441 return false;
2442 }
2443#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2444 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
2445 {
2446 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
2447 return false;
2448 }
2449 if (!check_list_argument(term[1], check_rule_SortExpr<atermpp::aterm>, 0))
2450 {
2451 mCRL2log(log::log_level_t::debug) << "check_rule_SortExpr" << std::endl;
2452 return false;
2453 }
2454#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2455
2456#endif // MCRL2_NO_SOUNDNESS_CHECKS
2457 return true;
2458}
2459
2460// Process(ProcVarId, DataExpr*)
2461template <atermpp::IsATerm Term>
2462bool check_term_Process([[maybe_unused]] const Term& t)
2463{
2464#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2465 // check the type of the term
2466 const atermpp::aterm& term(t);
2467 if (!term.type_is_appl())
2468 {
2469 return false;
2470 }
2471 if (term.function() != core::detail::function_symbols::Process)
2472 {
2473 return false;
2474 }
2475
2476 // check the children
2477 if (term.size() != 2)
2478 {
2479 return false;
2480 }
2481#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2482 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
2483 {
2484 mCRL2log(log::log_level_t::debug) << "check_rule_ProcVarId" << std::endl;
2485 return false;
2486 }
2487 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
2488 {
2489 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2490 return false;
2491 }
2492#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2493
2494#endif // MCRL2_NO_SOUNDNESS_CHECKS
2495 return true;
2496}
2497
2498// ProcessAssignment(ProcVarId, DataVarIdInit*)
2499template <atermpp::IsATerm Term>
2501{
2502#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2503 // check the type of the term
2504 const atermpp::aterm& term(t);
2505 if (!term.type_is_appl())
2506 {
2507 return false;
2508 }
2509 if (term.function() != core::detail::function_symbols::ProcessAssignment)
2510 {
2511 return false;
2512 }
2513
2514 // check the children
2515 if (term.size() != 2)
2516 {
2517 return false;
2518 }
2519#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2520 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
2521 {
2522 mCRL2log(log::log_level_t::debug) << "check_rule_ProcVarId" << std::endl;
2523 return false;
2524 }
2525 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
2526 {
2527 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarIdInit" << std::endl;
2528 return false;
2529 }
2530#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2531
2532#endif // MCRL2_NO_SOUNDNESS_CHECKS
2533 return true;
2534}
2535
2536// Delta()
2537template <atermpp::IsATerm Term>
2538bool check_term_Delta([[maybe_unused]] const Term& t)
2539{
2540#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2541 // check the type of the term
2542 const atermpp::aterm& term(t);
2543 if (!term.type_is_appl())
2544 {
2545 return false;
2546 }
2547 if (term.function() != core::detail::function_symbols::Delta)
2548 {
2549 return false;
2550 }
2551
2552 // check the children
2553 if (term.size() != 0)
2554 {
2555 return false;
2556 }
2557
2558#endif // MCRL2_NO_SOUNDNESS_CHECKS
2559 return true;
2560}
2561
2562// Tau()
2563template <atermpp::IsATerm Term>
2564bool check_term_Tau([[maybe_unused]] const Term& t)
2565{
2566#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2567 // check the type of the term
2568 const atermpp::aterm& term(t);
2569 if (!term.type_is_appl())
2570 {
2571 return false;
2572 }
2573 if (term.function() != core::detail::function_symbols::Tau)
2574 {
2575 return false;
2576 }
2577
2578 // check the children
2579 if (term.size() != 0)
2580 {
2581 return false;
2582 }
2583
2584#endif // MCRL2_NO_SOUNDNESS_CHECKS
2585 return true;
2586}
2587
2588// Sum(DataVarId+, ProcExpr)
2589template <atermpp::IsATerm Term>
2590bool check_term_Sum([[maybe_unused]] const Term& t)
2591{
2592#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2593 // check the type of the term
2594 const atermpp::aterm& term(t);
2595 if (!term.type_is_appl())
2596 {
2597 return false;
2598 }
2599 if (term.function() != core::detail::function_symbols::Sum)
2600 {
2601 return false;
2602 }
2603
2604 // check the children
2605 if (term.size() != 2)
2606 {
2607 return false;
2608 }
2609#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2610 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
2611 {
2612 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
2613 return false;
2614 }
2615 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2616 {
2617 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2618 return false;
2619 }
2620#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2621
2622#endif // MCRL2_NO_SOUNDNESS_CHECKS
2623 return true;
2624}
2625
2626// Block(String*, ProcExpr)
2627template <atermpp::IsATerm Term>
2628bool check_term_Block([[maybe_unused]] const Term& t)
2629{
2630#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2631 // check the type of the term
2632 const atermpp::aterm& term(t);
2633 if (!term.type_is_appl())
2634 {
2635 return false;
2636 }
2637 if (term.function() != core::detail::function_symbols::Block)
2638 {
2639 return false;
2640 }
2641
2642 // check the children
2643 if (term.size() != 2)
2644 {
2645 return false;
2646 }
2647#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2648 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 0))
2649 {
2650 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
2651 return false;
2652 }
2653 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2654 {
2655 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2656 return false;
2657 }
2658#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2659
2660#endif // MCRL2_NO_SOUNDNESS_CHECKS
2661 return true;
2662}
2663
2664// Hide(String*, ProcExpr)
2665template <atermpp::IsATerm Term>
2666bool check_term_Hide([[maybe_unused]] const Term& t)
2667{
2668#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2669 // check the type of the term
2670 const atermpp::aterm& term(t);
2671 if (!term.type_is_appl())
2672 {
2673 return false;
2674 }
2675 if (term.function() != core::detail::function_symbols::Hide)
2676 {
2677 return false;
2678 }
2679
2680 // check the children
2681 if (term.size() != 2)
2682 {
2683 return false;
2684 }
2685#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2686 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 0))
2687 {
2688 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
2689 return false;
2690 }
2691 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2692 {
2693 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2694 return false;
2695 }
2696#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2697
2698#endif // MCRL2_NO_SOUNDNESS_CHECKS
2699 return true;
2700}
2701
2702// Rename(RenameExpr*, ProcExpr)
2703template <atermpp::IsATerm Term>
2704bool check_term_Rename([[maybe_unused]] const Term& t)
2705{
2706#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2707 // check the type of the term
2708 const atermpp::aterm& term(t);
2709 if (!term.type_is_appl())
2710 {
2711 return false;
2712 }
2713 if (term.function() != core::detail::function_symbols::Rename)
2714 {
2715 return false;
2716 }
2717
2718 // check the children
2719 if (term.size() != 2)
2720 {
2721 return false;
2722 }
2723#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2724 if (!check_list_argument(term[0], check_rule_RenameExpr<atermpp::aterm>, 0))
2725 {
2726 mCRL2log(log::log_level_t::debug) << "check_rule_RenameExpr" << std::endl;
2727 return false;
2728 }
2729 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2730 {
2731 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2732 return false;
2733 }
2734#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2735
2736#endif // MCRL2_NO_SOUNDNESS_CHECKS
2737 return true;
2738}
2739
2740// Comm(CommExpr*, ProcExpr)
2741template <atermpp::IsATerm Term>
2742bool check_term_Comm([[maybe_unused]] const Term& t)
2743{
2744#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2745 // check the type of the term
2746 const atermpp::aterm& term(t);
2747 if (!term.type_is_appl())
2748 {
2749 return false;
2750 }
2751 if (term.function() != core::detail::function_symbols::Comm)
2752 {
2753 return false;
2754 }
2755
2756 // check the children
2757 if (term.size() != 2)
2758 {
2759 return false;
2760 }
2761#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2762 if (!check_list_argument(term[0], check_rule_CommExpr<atermpp::aterm>, 0))
2763 {
2764 mCRL2log(log::log_level_t::debug) << "check_rule_CommExpr" << std::endl;
2765 return false;
2766 }
2767 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2768 {
2769 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2770 return false;
2771 }
2772#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2773
2774#endif // MCRL2_NO_SOUNDNESS_CHECKS
2775 return true;
2776}
2777
2778// Allow(MultActName*, ProcExpr)
2779template <atermpp::IsATerm Term>
2780bool check_term_Allow([[maybe_unused]] const Term& t)
2781{
2782#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2783 // check the type of the term
2784 const atermpp::aterm& term(t);
2785 if (!term.type_is_appl())
2786 {
2787 return false;
2788 }
2789 if (term.function() != core::detail::function_symbols::Allow)
2790 {
2791 return false;
2792 }
2793
2794 // check the children
2795 if (term.size() != 2)
2796 {
2797 return false;
2798 }
2799#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2800 if (!check_list_argument(term[0], check_rule_MultActName<atermpp::aterm>, 0))
2801 {
2802 mCRL2log(log::log_level_t::debug) << "check_rule_MultActName" << std::endl;
2803 return false;
2804 }
2805 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2806 {
2807 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2808 return false;
2809 }
2810#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2811
2812#endif // MCRL2_NO_SOUNDNESS_CHECKS
2813 return true;
2814}
2815
2816// Sync(ProcExpr, ProcExpr)
2817template <atermpp::IsATerm Term>
2818bool check_term_Sync([[maybe_unused]] const Term& t)
2819{
2820#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2821 // check the type of the term
2822 const atermpp::aterm& term(t);
2823 if (!term.type_is_appl())
2824 {
2825 return false;
2826 }
2827 if (term.function() != core::detail::function_symbols::Sync)
2828 {
2829 return false;
2830 }
2831
2832 // check the children
2833 if (term.size() != 2)
2834 {
2835 return false;
2836 }
2837#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2838 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2839 {
2840 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2841 return false;
2842 }
2843 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2844 {
2845 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2846 return false;
2847 }
2848#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2849
2850#endif // MCRL2_NO_SOUNDNESS_CHECKS
2851 return true;
2852}
2853
2854// AtTime(ProcExpr, DataExpr)
2855template <atermpp::IsATerm Term>
2856bool check_term_AtTime([[maybe_unused]] const Term& t)
2857{
2858#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2859 // check the type of the term
2860 const atermpp::aterm& term(t);
2861 if (!term.type_is_appl())
2862 {
2863 return false;
2864 }
2865 if (term.function() != core::detail::function_symbols::AtTime)
2866 {
2867 return false;
2868 }
2869
2870 // check the children
2871 if (term.size() != 2)
2872 {
2873 return false;
2874 }
2875#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2876 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2877 {
2878 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2879 return false;
2880 }
2881 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2882 {
2883 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2884 return false;
2885 }
2886#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2887
2888#endif // MCRL2_NO_SOUNDNESS_CHECKS
2889 return true;
2890}
2891
2892// Seq(ProcExpr, ProcExpr)
2893template <atermpp::IsATerm Term>
2894bool check_term_Seq([[maybe_unused]] const Term& t)
2895{
2896#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2897 // check the type of the term
2898 const atermpp::aterm& term(t);
2899 if (!term.type_is_appl())
2900 {
2901 return false;
2902 }
2903 if (term.function() != core::detail::function_symbols::Seq)
2904 {
2905 return false;
2906 }
2907
2908 // check the children
2909 if (term.size() != 2)
2910 {
2911 return false;
2912 }
2913#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2914 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2915 {
2916 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2917 return false;
2918 }
2919 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2920 {
2921 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2922 return false;
2923 }
2924#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2925
2926#endif // MCRL2_NO_SOUNDNESS_CHECKS
2927 return true;
2928}
2929
2930// IfThen(DataExpr, ProcExpr)
2931template <atermpp::IsATerm Term>
2932bool check_term_IfThen([[maybe_unused]] const Term& t)
2933{
2934#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2935 // check the type of the term
2936 const atermpp::aterm& term(t);
2937 if (!term.type_is_appl())
2938 {
2939 return false;
2940 }
2941 if (term.function() != core::detail::function_symbols::IfThen)
2942 {
2943 return false;
2944 }
2945
2946 // check the children
2947 if (term.size() != 2)
2948 {
2949 return false;
2950 }
2951#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2952 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
2953 {
2954 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2955 return false;
2956 }
2957 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2958 {
2959 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2960 return false;
2961 }
2962#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2963
2964#endif // MCRL2_NO_SOUNDNESS_CHECKS
2965 return true;
2966}
2967
2968// IfThenElse(DataExpr, ProcExpr, ProcExpr)
2969template <atermpp::IsATerm Term>
2971{
2972#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2973 // check the type of the term
2974 const atermpp::aterm& term(t);
2975 if (!term.type_is_appl())
2976 {
2977 return false;
2978 }
2979 if (term.function() != core::detail::function_symbols::IfThenElse)
2980 {
2981 return false;
2982 }
2983
2984 // check the children
2985 if (term.size() != 3)
2986 {
2987 return false;
2988 }
2989#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2990 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
2991 {
2992 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
2993 return false;
2994 }
2995 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2996 {
2997 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
2998 return false;
2999 }
3000 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3001 {
3002 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3003 return false;
3004 }
3005#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3006
3007#endif // MCRL2_NO_SOUNDNESS_CHECKS
3008 return true;
3009}
3010
3011// BInit(ProcExpr, ProcExpr)
3012template <atermpp::IsATerm Term>
3013bool check_term_BInit([[maybe_unused]] const Term& t)
3014{
3015#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3016 // check the type of the term
3017 const atermpp::aterm& term(t);
3018 if (!term.type_is_appl())
3019 {
3020 return false;
3021 }
3022 if (term.function() != core::detail::function_symbols::BInit)
3023 {
3024 return false;
3025 }
3026
3027 // check the children
3028 if (term.size() != 2)
3029 {
3030 return false;
3031 }
3032#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3033 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3034 {
3035 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3036 return false;
3037 }
3038 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3039 {
3040 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3041 return false;
3042 }
3043#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3044
3045#endif // MCRL2_NO_SOUNDNESS_CHECKS
3046 return true;
3047}
3048
3049// Merge(ProcExpr, ProcExpr)
3050template <atermpp::IsATerm Term>
3051bool check_term_Merge([[maybe_unused]] const Term& t)
3052{
3053#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3054 // check the type of the term
3055 const atermpp::aterm& term(t);
3056 if (!term.type_is_appl())
3057 {
3058 return false;
3059 }
3060 if (term.function() != core::detail::function_symbols::Merge)
3061 {
3062 return false;
3063 }
3064
3065 // check the children
3066 if (term.size() != 2)
3067 {
3068 return false;
3069 }
3070#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3071 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3072 {
3073 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3074 return false;
3075 }
3076 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3077 {
3078 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3079 return false;
3080 }
3081#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3082
3083#endif // MCRL2_NO_SOUNDNESS_CHECKS
3084 return true;
3085}
3086
3087// LMerge(ProcExpr, ProcExpr)
3088template <atermpp::IsATerm Term>
3089bool check_term_LMerge([[maybe_unused]] const Term& t)
3090{
3091#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3092 // check the type of the term
3093 const atermpp::aterm& term(t);
3094 if (!term.type_is_appl())
3095 {
3096 return false;
3097 }
3098 if (term.function() != core::detail::function_symbols::LMerge)
3099 {
3100 return false;
3101 }
3102
3103 // check the children
3104 if (term.size() != 2)
3105 {
3106 return false;
3107 }
3108#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3109 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3110 {
3111 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3112 return false;
3113 }
3114 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3115 {
3116 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3117 return false;
3118 }
3119#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3120
3121#endif // MCRL2_NO_SOUNDNESS_CHECKS
3122 return true;
3123}
3124
3125// Choice(ProcExpr, ProcExpr)
3126template <atermpp::IsATerm Term>
3127bool check_term_Choice([[maybe_unused]] const Term& t)
3128{
3129#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3130 // check the type of the term
3131 const atermpp::aterm& term(t);
3132 if (!term.type_is_appl())
3133 {
3134 return false;
3135 }
3136 if (term.function() != core::detail::function_symbols::Choice)
3137 {
3138 return false;
3139 }
3140
3141 // check the children
3142 if (term.size() != 2)
3143 {
3144 return false;
3145 }
3146#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3147 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3148 {
3149 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3150 return false;
3151 }
3152 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3153 {
3154 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3155 return false;
3156 }
3157#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3158
3159#endif // MCRL2_NO_SOUNDNESS_CHECKS
3160 return true;
3161}
3162
3163// StochasticOperator(DataVarId+, DataExpr, ProcExpr)
3164template <atermpp::IsATerm Term>
3166{
3167#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3168 // check the type of the term
3169 const atermpp::aterm& term(t);
3170 if (!term.type_is_appl())
3171 {
3172 return false;
3173 }
3174 if (term.function() != core::detail::function_symbols::StochasticOperator)
3175 {
3176 return false;
3177 }
3178
3179 // check the children
3180 if (term.size() != 3)
3181 {
3182 return false;
3183 }
3184#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3185 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
3186 {
3187 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
3188 return false;
3189 }
3190 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3191 {
3192 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
3193 return false;
3194 }
3195 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3196 {
3197 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3198 return false;
3199 }
3200#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3201
3202#endif // MCRL2_NO_SOUNDNESS_CHECKS
3203 return true;
3204}
3205
3206// UntypedProcessAssignment(String, UntypedIdentifierAssignment*)
3207template <atermpp::IsATerm Term>
3209{
3210#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3211 // check the type of the term
3212 const atermpp::aterm& term(t);
3213 if (!term.type_is_appl())
3214 {
3215 return false;
3216 }
3217 if (term.function() != core::detail::function_symbols::UntypedProcessAssignment)
3218 {
3219 return false;
3220 }
3221
3222 // check the children
3223 if (term.size() != 2)
3224 {
3225 return false;
3226 }
3227#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3228 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3229 {
3230 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
3231 return false;
3232 }
3233 if (!check_list_argument(term[1], check_rule_UntypedIdentifierAssignment<atermpp::aterm>, 0))
3234 {
3235 mCRL2log(log::log_level_t::debug) << "check_rule_UntypedIdentifierAssignment" << std::endl;
3236 return false;
3237 }
3238#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3239
3240#endif // MCRL2_NO_SOUNDNESS_CHECKS
3241 return true;
3242}
3243
3244// ProcVarId(String, DataVarId*)
3245template <atermpp::IsATerm Term>
3246bool check_term_ProcVarId([[maybe_unused]] const Term& t)
3247{
3248#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3249 // check the type of the term
3250 const atermpp::aterm& term(t);
3251 if (!term.type_is_appl())
3252 {
3253 return false;
3254 }
3255 if (term.function() != core::detail::function_symbols::ProcVarId)
3256 {
3257 return false;
3258 }
3259
3260 // check the children
3261 if (term.size() != 2)
3262 {
3263 return false;
3264 }
3265#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3266 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3267 {
3268 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
3269 return false;
3270 }
3271 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
3272 {
3273 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
3274 return false;
3275 }
3276#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3277
3278#endif // MCRL2_NO_SOUNDNESS_CHECKS
3279 return true;
3280}
3281
3282// MultActName(String+)
3283template <atermpp::IsATerm Term>
3285{
3286#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3287 // check the type of the term
3288 const atermpp::aterm& term(t);
3289 if (!term.type_is_appl())
3290 {
3291 return false;
3292 }
3293 if (term.function() != core::detail::function_symbols::MultActName)
3294 {
3295 return false;
3296 }
3297
3298 // check the children
3299 if (term.size() != 1)
3300 {
3301 return false;
3302 }
3303#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3304 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 1))
3305 {
3306 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
3307 return false;
3308 }
3309#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3310
3311#endif // MCRL2_NO_SOUNDNESS_CHECKS
3312 return true;
3313}
3314
3315// RenameExpr(String, String)
3316template <atermpp::IsATerm Term>
3318{
3319#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3320 // check the type of the term
3321 const atermpp::aterm& term(t);
3322 if (!term.type_is_appl())
3323 {
3324 return false;
3325 }
3326 if (term.function() != core::detail::function_symbols::RenameExpr)
3327 {
3328 return false;
3329 }
3330
3331 // check the children
3332 if (term.size() != 2)
3333 {
3334 return false;
3335 }
3336#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3337 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3338 {
3339 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
3340 return false;
3341 }
3342 if (!check_term_argument(term[1], check_rule_String<atermpp::aterm>))
3343 {
3344 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
3345 return false;
3346 }
3347#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3348
3349#endif // MCRL2_NO_SOUNDNESS_CHECKS
3350 return true;
3351}
3352
3353// CommExpr(MultActName, String)
3354template <atermpp::IsATerm Term>
3355bool check_term_CommExpr([[maybe_unused]] const Term& t)
3356{
3357#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3358 // check the type of the term
3359 const atermpp::aterm& term(t);
3360 if (!term.type_is_appl())
3361 {
3362 return false;
3363 }
3364 if (term.function() != core::detail::function_symbols::CommExpr)
3365 {
3366 return false;
3367 }
3368
3369 // check the children
3370 if (term.size() != 2)
3371 {
3372 return false;
3373 }
3374#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3375 if (!check_term_argument(term[0], check_rule_MultActName<atermpp::aterm>))
3376 {
3377 mCRL2log(log::log_level_t::debug) << "check_rule_MultActName" << std::endl;
3378 return false;
3379 }
3380 if (!check_term_argument(term[1], check_rule_String<atermpp::aterm>))
3381 {
3382 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
3383 return false;
3384 }
3385#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3386
3387#endif // MCRL2_NO_SOUNDNESS_CHECKS
3388 return true;
3389}
3390
3391// ProcSpec(DataSpec, ActSpec, GlobVarSpec, ProcEqnSpec, ProcInit)
3392template <atermpp::IsATerm Term>
3393bool check_term_ProcSpec([[maybe_unused]] const Term& t)
3394{
3395#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3396 // check the type of the term
3397 const atermpp::aterm& term(t);
3398 if (!term.type_is_appl())
3399 {
3400 return false;
3401 }
3402 if (term.function() != core::detail::function_symbols::ProcSpec)
3403 {
3404 return false;
3405 }
3406
3407 // check the children
3408 if (term.size() != 5)
3409 {
3410 return false;
3411 }
3412#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3413 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
3414 {
3415 mCRL2log(log::log_level_t::debug) << "check_rule_DataSpec" << std::endl;
3416 return false;
3417 }
3418 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
3419 {
3420 mCRL2log(log::log_level_t::debug) << "check_rule_ActSpec" << std::endl;
3421 return false;
3422 }
3423 if (!check_term_argument(term[2], check_rule_GlobVarSpec<atermpp::aterm>))
3424 {
3425 mCRL2log(log::log_level_t::debug) << "check_rule_GlobVarSpec" << std::endl;
3426 return false;
3427 }
3428 if (!check_term_argument(term[3], check_rule_ProcEqnSpec<atermpp::aterm>))
3429 {
3430 mCRL2log(log::log_level_t::debug) << "check_rule_ProcEqnSpec" << std::endl;
3431 return false;
3432 }
3433 if (!check_term_argument(term[4], check_rule_ProcInit<atermpp::aterm>))
3434 {
3435 mCRL2log(log::log_level_t::debug) << "check_rule_ProcInit" << std::endl;
3436 return false;
3437 }
3438#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3439
3440#endif // MCRL2_NO_SOUNDNESS_CHECKS
3441 return true;
3442}
3443
3444// ActSpec(ActId*)
3445template <atermpp::IsATerm Term>
3446bool check_term_ActSpec([[maybe_unused]] const Term& t)
3447{
3448#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3449 // check the type of the term
3450 const atermpp::aterm& term(t);
3451 if (!term.type_is_appl())
3452 {
3453 return false;
3454 }
3455 if (term.function() != core::detail::function_symbols::ActSpec)
3456 {
3457 return false;
3458 }
3459
3460 // check the children
3461 if (term.size() != 1)
3462 {
3463 return false;
3464 }
3465#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3466 if (!check_list_argument(term[0], check_rule_ActId<atermpp::aterm>, 0))
3467 {
3468 mCRL2log(log::log_level_t::debug) << "check_rule_ActId" << std::endl;
3469 return false;
3470 }
3471#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3472
3473#endif // MCRL2_NO_SOUNDNESS_CHECKS
3474 return true;
3475}
3476
3477// GlobVarSpec(DataVarId*)
3478template <atermpp::IsATerm Term>
3480{
3481#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3482 // check the type of the term
3483 const atermpp::aterm& term(t);
3484 if (!term.type_is_appl())
3485 {
3486 return false;
3487 }
3488 if (term.function() != core::detail::function_symbols::GlobVarSpec)
3489 {
3490 return false;
3491 }
3492
3493 // check the children
3494 if (term.size() != 1)
3495 {
3496 return false;
3497 }
3498#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3499 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3500 {
3501 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
3502 return false;
3503 }
3504#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3505
3506#endif // MCRL2_NO_SOUNDNESS_CHECKS
3507 return true;
3508}
3509
3510// ProcEqnSpec(ProcEqn*)
3511template <atermpp::IsATerm Term>
3513{
3514#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3515 // check the type of the term
3516 const atermpp::aterm& term(t);
3517 if (!term.type_is_appl())
3518 {
3519 return false;
3520 }
3521 if (term.function() != core::detail::function_symbols::ProcEqnSpec)
3522 {
3523 return false;
3524 }
3525
3526 // check the children
3527 if (term.size() != 1)
3528 {
3529 return false;
3530 }
3531#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3532 if (!check_list_argument(term[0], check_rule_ProcEqn<atermpp::aterm>, 0))
3533 {
3534 mCRL2log(log::log_level_t::debug) << "check_rule_ProcEqn" << std::endl;
3535 return false;
3536 }
3537#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3538
3539#endif // MCRL2_NO_SOUNDNESS_CHECKS
3540 return true;
3541}
3542
3543// ProcEqn(ProcVarId, DataVarId*, ProcExpr)
3544template <atermpp::IsATerm Term>
3545bool check_term_ProcEqn([[maybe_unused]] const Term& t)
3546{
3547#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3548 // check the type of the term
3549 const atermpp::aterm& term(t);
3550 if (!term.type_is_appl())
3551 {
3552 return false;
3553 }
3554 if (term.function() != core::detail::function_symbols::ProcEqn)
3555 {
3556 return false;
3557 }
3558
3559 // check the children
3560 if (term.size() != 3)
3561 {
3562 return false;
3563 }
3564#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3565 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
3566 {
3567 mCRL2log(log::log_level_t::debug) << "check_rule_ProcVarId" << std::endl;
3568 return false;
3569 }
3570 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
3571 {
3572 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
3573 return false;
3574 }
3575 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3576 {
3577 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3578 return false;
3579 }
3580#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3581
3582#endif // MCRL2_NO_SOUNDNESS_CHECKS
3583 return true;
3584}
3585
3586// ProcessInit(ProcExpr)
3587template <atermpp::IsATerm Term>
3589{
3590#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3591 // check the type of the term
3592 const atermpp::aterm& term(t);
3593 if (!term.type_is_appl())
3594 {
3595 return false;
3596 }
3597 if (term.function() != core::detail::function_symbols::ProcessInit)
3598 {
3599 return false;
3600 }
3601
3602 // check the children
3603 if (term.size() != 1)
3604 {
3605 return false;
3606 }
3607#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3608 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3609 {
3610 mCRL2log(log::log_level_t::debug) << "check_rule_ProcExpr" << std::endl;
3611 return false;
3612 }
3613#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3614
3615#endif // MCRL2_NO_SOUNDNESS_CHECKS
3616 return true;
3617}
3618
3619// Distribution(DataVarId*, DataExpr)
3620template <atermpp::IsATerm Term>
3622{
3623#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3624 // check the type of the term
3625 const atermpp::aterm& term(t);
3626 if (!term.type_is_appl())
3627 {
3628 return false;
3629 }
3630 if (term.function() != core::detail::function_symbols::Distribution)
3631 {
3632 return false;
3633 }
3634
3635 // check the children
3636 if (term.size() != 2)
3637 {
3638 return false;
3639 }
3640#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3641 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3642 {
3643 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
3644 return false;
3645 }
3646 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3647 {
3648 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
3649 return false;
3650 }
3651#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3652
3653#endif // MCRL2_NO_SOUNDNESS_CHECKS
3654 return true;
3655}
3656
3657// LinProcSpec(DataSpec, ActSpec, GlobVarSpec, LinearProcess, LinearProcessInit)
3658template <atermpp::IsATerm Term>
3660{
3661#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3662 // check the type of the term
3663 const atermpp::aterm& term(t);
3664 if (!term.type_is_appl())
3665 {
3666 return false;
3667 }
3668 if (term.function() != core::detail::function_symbols::LinProcSpec)
3669 {
3670 return false;
3671 }
3672
3673 // check the children
3674 if (term.size() != 5)
3675 {
3676 return false;
3677 }
3678#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3679 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
3680 {
3681 mCRL2log(log::log_level_t::debug) << "check_rule_DataSpec" << std::endl;
3682 return false;
3683 }
3684 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
3685 {
3686 mCRL2log(log::log_level_t::debug) << "check_rule_ActSpec" << std::endl;
3687 return false;
3688 }
3689 if (!check_term_argument(term[2], check_rule_GlobVarSpec<atermpp::aterm>))
3690 {
3691 mCRL2log(log::log_level_t::debug) << "check_rule_GlobVarSpec" << std::endl;
3692 return false;
3693 }
3694 if (!check_term_argument(term[3], check_rule_LinearProcess<atermpp::aterm>))
3695 {
3696 mCRL2log(log::log_level_t::debug) << "check_rule_LinearProcess" << std::endl;
3697 return false;
3698 }
3699 if (!check_term_argument(term[4], check_rule_LinearProcessInit<atermpp::aterm>))
3700 {
3701 mCRL2log(log::log_level_t::debug) << "check_rule_LinearProcessInit" << std::endl;
3702 return false;
3703 }
3704#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3705
3706#endif // MCRL2_NO_SOUNDNESS_CHECKS
3707 return true;
3708}
3709
3710// LinearProcess(DataVarId*, LinearProcessSummand*)
3711template <atermpp::IsATerm Term>
3713{
3714#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3715 // check the type of the term
3716 const atermpp::aterm& term(t);
3717 if (!term.type_is_appl())
3718 {
3719 return false;
3720 }
3721 if (term.function() != core::detail::function_symbols::LinearProcess)
3722 {
3723 return false;
3724 }
3725
3726 // check the children
3727 if (term.size() != 2)
3728 {
3729 return false;
3730 }
3731#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3732 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3733 {
3734 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
3735 return false;
3736 }
3737 if (!check_list_argument(term[1], check_rule_LinearProcessSummand<atermpp::aterm>, 0))
3738 {
3739 mCRL2log(log::log_level_t::debug) << "check_rule_LinearProcessSummand" << std::endl;
3740 return false;
3741 }
3742#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3743
3744#endif // MCRL2_NO_SOUNDNESS_CHECKS
3745 return true;
3746}
3747
3748// LinearProcessSummand(DataVarId*, DataExpr, MultActOrDelta, DataExpr, DataVarIdInit*, Distribution)
3749template <atermpp::IsATerm Term>
3751{
3752#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3753 // check the type of the term
3754 const atermpp::aterm& term(t);
3755 if (!term.type_is_appl())
3756 {
3757 return false;
3758 }
3759 if (term.function() != core::detail::function_symbols::LinearProcessSummand)
3760 {
3761 return false;
3762 }
3763
3764 // check the children
3765 if (term.size() != 6)
3766 {
3767 return false;
3768 }
3769#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3770 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3771 {
3772 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
3773 return false;
3774 }
3775 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3776 {
3777 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
3778 return false;
3779 }
3780 if (!check_term_argument(term[2], check_rule_MultActOrDelta<atermpp::aterm>))
3781 {
3782 mCRL2log(log::log_level_t::debug) << "check_rule_MultActOrDelta" << std::endl;
3783 return false;
3784 }
3785 if (!check_term_argument(term[3], check_rule_DataExpr<atermpp::aterm>))
3786 {
3787 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
3788 return false;
3789 }
3790 if (!check_list_argument(term[4], check_rule_DataVarIdInit<atermpp::aterm>, 0))
3791 {
3792 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarIdInit" << std::endl;
3793 return false;
3794 }
3795 if (!check_term_argument(term[5], check_rule_Distribution<atermpp::aterm>))
3796 {
3797 mCRL2log(log::log_level_t::debug) << "check_rule_Distribution" << std::endl;
3798 return false;
3799 }
3800#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3801
3802#endif // MCRL2_NO_SOUNDNESS_CHECKS
3803 return true;
3804}
3805
3806// LinearProcessInit(DataExpr*, Distribution)
3807template <atermpp::IsATerm Term>
3809{
3810#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3811 // check the type of the term
3812 const atermpp::aterm& term(t);
3813 if (!term.type_is_appl())
3814 {
3815 return false;
3816 }
3817 if (term.function() != core::detail::function_symbols::LinearProcessInit)
3818 {
3819 return false;
3820 }
3821
3822 // check the children
3823 if (term.size() != 2)
3824 {
3825 return false;
3826 }
3827#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3828 if (!check_list_argument(term[0], check_rule_DataExpr<atermpp::aterm>, 0))
3829 {
3830 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
3831 return false;
3832 }
3833 if (!check_term_argument(term[1], check_rule_Distribution<atermpp::aterm>))
3834 {
3835 mCRL2log(log::log_level_t::debug) << "check_rule_Distribution" << std::endl;
3836 return false;
3837 }
3838#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3839
3840#endif // MCRL2_NO_SOUNDNESS_CHECKS
3841 return true;
3842}
3843
3844// StateTrue()
3845template <atermpp::IsATerm Term>
3846bool check_term_StateTrue([[maybe_unused]] const Term& t)
3847{
3848#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3849 // check the type of the term
3850 const atermpp::aterm& term(t);
3851 if (!term.type_is_appl())
3852 {
3853 return false;
3854 }
3855 if (term.function() != core::detail::function_symbols::StateTrue)
3856 {
3857 return false;
3858 }
3859
3860 // check the children
3861 if (term.size() != 0)
3862 {
3863 return false;
3864 }
3865
3866#endif // MCRL2_NO_SOUNDNESS_CHECKS
3867 return true;
3868}
3869
3870// StateFalse()
3871template <atermpp::IsATerm Term>
3873{
3874#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3875 // check the type of the term
3876 const atermpp::aterm& term(t);
3877 if (!term.type_is_appl())
3878 {
3879 return false;
3880 }
3881 if (term.function() != core::detail::function_symbols::StateFalse)
3882 {
3883 return false;
3884 }
3885
3886 // check the children
3887 if (term.size() != 0)
3888 {
3889 return false;
3890 }
3891
3892#endif // MCRL2_NO_SOUNDNESS_CHECKS
3893 return true;
3894}
3895
3896// StateNot(StateFrm)
3897template <atermpp::IsATerm Term>
3898bool check_term_StateNot([[maybe_unused]] const Term& t)
3899{
3900#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3901 // check the type of the term
3902 const atermpp::aterm& term(t);
3903 if (!term.type_is_appl())
3904 {
3905 return false;
3906 }
3907 if (term.function() != core::detail::function_symbols::StateNot)
3908 {
3909 return false;
3910 }
3911
3912 // check the children
3913 if (term.size() != 1)
3914 {
3915 return false;
3916 }
3917#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3918 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
3919 {
3920 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
3921 return false;
3922 }
3923#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3924
3925#endif // MCRL2_NO_SOUNDNESS_CHECKS
3926 return true;
3927}
3928
3929// StateMinus(StateFrm)
3930template <atermpp::IsATerm Term>
3932{
3933#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3934 // check the type of the term
3935 const atermpp::aterm& term(t);
3936 if (!term.type_is_appl())
3937 {
3938 return false;
3939 }
3940 if (term.function() != core::detail::function_symbols::StateMinus)
3941 {
3942 return false;
3943 }
3944
3945 // check the children
3946 if (term.size() != 1)
3947 {
3948 return false;
3949 }
3950#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3951 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
3952 {
3953 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
3954 return false;
3955 }
3956#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3957
3958#endif // MCRL2_NO_SOUNDNESS_CHECKS
3959 return true;
3960}
3961
3962// StateAnd(StateFrm, StateFrm)
3963template <atermpp::IsATerm Term>
3964bool check_term_StateAnd([[maybe_unused]] const Term& t)
3965{
3966#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3967 // check the type of the term
3968 const atermpp::aterm& term(t);
3969 if (!term.type_is_appl())
3970 {
3971 return false;
3972 }
3973 if (term.function() != core::detail::function_symbols::StateAnd)
3974 {
3975 return false;
3976 }
3977
3978 // check the children
3979 if (term.size() != 2)
3980 {
3981 return false;
3982 }
3983#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3984 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
3985 {
3986 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
3987 return false;
3988 }
3989 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
3990 {
3991 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
3992 return false;
3993 }
3994#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3995
3996#endif // MCRL2_NO_SOUNDNESS_CHECKS
3997 return true;
3998}
3999
4000// StateOr(StateFrm, StateFrm)
4001template <atermpp::IsATerm Term>
4002bool check_term_StateOr([[maybe_unused]] const Term& t)
4003{
4004#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4005 // check the type of the term
4006 const atermpp::aterm& term(t);
4007 if (!term.type_is_appl())
4008 {
4009 return false;
4010 }
4011 if (term.function() != core::detail::function_symbols::StateOr)
4012 {
4013 return false;
4014 }
4015
4016 // check the children
4017 if (term.size() != 2)
4018 {
4019 return false;
4020 }
4021#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4022 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4023 {
4024 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4025 return false;
4026 }
4027 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4028 {
4029 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4030 return false;
4031 }
4032#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4033
4034#endif // MCRL2_NO_SOUNDNESS_CHECKS
4035 return true;
4036}
4037
4038// StateImp(StateFrm, StateFrm)
4039template <atermpp::IsATerm Term>
4040bool check_term_StateImp([[maybe_unused]] const Term& t)
4041{
4042#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4043 // check the type of the term
4044 const atermpp::aterm& term(t);
4045 if (!term.type_is_appl())
4046 {
4047 return false;
4048 }
4049 if (term.function() != core::detail::function_symbols::StateImp)
4050 {
4051 return false;
4052 }
4053
4054 // check the children
4055 if (term.size() != 2)
4056 {
4057 return false;
4058 }
4059#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4060 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4061 {
4062 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4063 return false;
4064 }
4065 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4066 {
4067 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4068 return false;
4069 }
4070#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4071
4072#endif // MCRL2_NO_SOUNDNESS_CHECKS
4073 return true;
4074}
4075
4076// StatePlus(StateFrm, StateFrm)
4077template <atermpp::IsATerm Term>
4078bool check_term_StatePlus([[maybe_unused]] const Term& t)
4079{
4080#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4081 // check the type of the term
4082 const atermpp::aterm& term(t);
4083 if (!term.type_is_appl())
4084 {
4085 return false;
4086 }
4087 if (term.function() != core::detail::function_symbols::StatePlus)
4088 {
4089 return false;
4090 }
4091
4092 // check the children
4093 if (term.size() != 2)
4094 {
4095 return false;
4096 }
4097#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4098 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4099 {
4100 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4101 return false;
4102 }
4103 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4104 {
4105 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4106 return false;
4107 }
4108#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4109
4110#endif // MCRL2_NO_SOUNDNESS_CHECKS
4111 return true;
4112}
4113
4114// StateConstantMultiply(DataExpr, StateFrm)
4115template <atermpp::IsATerm Term>
4117{
4118#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4119 // check the type of the term
4120 const atermpp::aterm& term(t);
4121 if (!term.type_is_appl())
4122 {
4123 return false;
4124 }
4125 if (term.function() != core::detail::function_symbols::StateConstantMultiply)
4126 {
4127 return false;
4128 }
4129
4130 // check the children
4131 if (term.size() != 2)
4132 {
4133 return false;
4134 }
4135#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4136 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4137 {
4138 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
4139 return false;
4140 }
4141 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4142 {
4143 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4144 return false;
4145 }
4146#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4147
4148#endif // MCRL2_NO_SOUNDNESS_CHECKS
4149 return true;
4150}
4151
4152// StateConstantMultiplyAlt(StateFrm, DataExpr)
4153template <atermpp::IsATerm Term>
4155{
4156#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4157 // check the type of the term
4158 const atermpp::aterm& term(t);
4159 if (!term.type_is_appl())
4160 {
4161 return false;
4162 }
4163 if (term.function() != core::detail::function_symbols::StateConstantMultiplyAlt)
4164 {
4165 return false;
4166 }
4167
4168 // check the children
4169 if (term.size() != 2)
4170 {
4171 return false;
4172 }
4173#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4174 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4175 {
4176 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4177 return false;
4178 }
4179 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
4180 {
4181 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
4182 return false;
4183 }
4184#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4185
4186#endif // MCRL2_NO_SOUNDNESS_CHECKS
4187 return true;
4188}
4189
4190// StateForall(DataVarId+, StateFrm)
4191template <atermpp::IsATerm Term>
4193{
4194#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4195 // check the type of the term
4196 const atermpp::aterm& term(t);
4197 if (!term.type_is_appl())
4198 {
4199 return false;
4200 }
4201 if (term.function() != core::detail::function_symbols::StateForall)
4202 {
4203 return false;
4204 }
4205
4206 // check the children
4207 if (term.size() != 2)
4208 {
4209 return false;
4210 }
4211#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4212 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4213 {
4214 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
4215 return false;
4216 }
4217 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4218 {
4219 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4220 return false;
4221 }
4222#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4223
4224#endif // MCRL2_NO_SOUNDNESS_CHECKS
4225 return true;
4226}
4227
4228// StateExists(DataVarId+, StateFrm)
4229template <atermpp::IsATerm Term>
4231{
4232#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4233 // check the type of the term
4234 const atermpp::aterm& term(t);
4235 if (!term.type_is_appl())
4236 {
4237 return false;
4238 }
4239 if (term.function() != core::detail::function_symbols::StateExists)
4240 {
4241 return false;
4242 }
4243
4244 // check the children
4245 if (term.size() != 2)
4246 {
4247 return false;
4248 }
4249#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4250 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4251 {
4252 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
4253 return false;
4254 }
4255 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4256 {
4257 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4258 return false;
4259 }
4260#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4261
4262#endif // MCRL2_NO_SOUNDNESS_CHECKS
4263 return true;
4264}
4265
4266// StateInfimum(DataVarId+, StateFrm)
4267template <atermpp::IsATerm Term>
4269{
4270#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4271 // check the type of the term
4272 const atermpp::aterm& term(t);
4273 if (!term.type_is_appl())
4274 {
4275 return false;
4276 }
4277 if (term.function() != core::detail::function_symbols::StateInfimum)
4278 {
4279 return false;
4280 }
4281
4282 // check the children
4283 if (term.size() != 2)
4284 {
4285 return false;
4286 }
4287#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4288 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4289 {
4290 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
4291 return false;
4292 }
4293 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4294 {
4295 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4296 return false;
4297 }
4298#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4299
4300#endif // MCRL2_NO_SOUNDNESS_CHECKS
4301 return true;
4302}
4303
4304// StateSupremum(DataVarId+, StateFrm)
4305template <atermpp::IsATerm Term>
4307{
4308#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4309 // check the type of the term
4310 const atermpp::aterm& term(t);
4311 if (!term.type_is_appl())
4312 {
4313 return false;
4314 }
4315 if (term.function() != core::detail::function_symbols::StateSupremum)
4316 {
4317 return false;
4318 }
4319
4320 // check the children
4321 if (term.size() != 2)
4322 {
4323 return false;
4324 }
4325#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4326 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4327 {
4328 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
4329 return false;
4330 }
4331 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4332 {
4333 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4334 return false;
4335 }
4336#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4337
4338#endif // MCRL2_NO_SOUNDNESS_CHECKS
4339 return true;
4340}
4341
4342// StateSum(DataVarId+, StateFrm)
4343template <atermpp::IsATerm Term>
4344bool check_term_StateSum([[maybe_unused]] const Term& t)
4345{
4346#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4347 // check the type of the term
4348 const atermpp::aterm& term(t);
4349 if (!term.type_is_appl())
4350 {
4351 return false;
4352 }
4353 if (term.function() != core::detail::function_symbols::StateSum)
4354 {
4355 return false;
4356 }
4357
4358 // check the children
4359 if (term.size() != 2)
4360 {
4361 return false;
4362 }
4363#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4364 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4365 {
4366 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
4367 return false;
4368 }
4369 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4370 {
4371 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4372 return false;
4373 }
4374#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4375
4376#endif // MCRL2_NO_SOUNDNESS_CHECKS
4377 return true;
4378}
4379
4380// StateMust(RegFrm, StateFrm)
4381template <atermpp::IsATerm Term>
4382bool check_term_StateMust([[maybe_unused]] const Term& t)
4383{
4384#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4385 // check the type of the term
4386 const atermpp::aterm& term(t);
4387 if (!term.type_is_appl())
4388 {
4389 return false;
4390 }
4391 if (term.function() != core::detail::function_symbols::StateMust)
4392 {
4393 return false;
4394 }
4395
4396 // check the children
4397 if (term.size() != 2)
4398 {
4399 return false;
4400 }
4401#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4402 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4403 {
4404 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4405 return false;
4406 }
4407 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4408 {
4409 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4410 return false;
4411 }
4412#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4413
4414#endif // MCRL2_NO_SOUNDNESS_CHECKS
4415 return true;
4416}
4417
4418// StateMay(RegFrm, StateFrm)
4419template <atermpp::IsATerm Term>
4420bool check_term_StateMay([[maybe_unused]] const Term& t)
4421{
4422#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4423 // check the type of the term
4424 const atermpp::aterm& term(t);
4425 if (!term.type_is_appl())
4426 {
4427 return false;
4428 }
4429 if (term.function() != core::detail::function_symbols::StateMay)
4430 {
4431 return false;
4432 }
4433
4434 // check the children
4435 if (term.size() != 2)
4436 {
4437 return false;
4438 }
4439#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4440 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4441 {
4442 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4443 return false;
4444 }
4445 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4446 {
4447 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4448 return false;
4449 }
4450#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4451
4452#endif // MCRL2_NO_SOUNDNESS_CHECKS
4453 return true;
4454}
4455
4456// StateYaled()
4457template <atermpp::IsATerm Term>
4459{
4460#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4461 // check the type of the term
4462 const atermpp::aterm& term(t);
4463 if (!term.type_is_appl())
4464 {
4465 return false;
4466 }
4467 if (term.function() != core::detail::function_symbols::StateYaled)
4468 {
4469 return false;
4470 }
4471
4472 // check the children
4473 if (term.size() != 0)
4474 {
4475 return false;
4476 }
4477
4478#endif // MCRL2_NO_SOUNDNESS_CHECKS
4479 return true;
4480}
4481
4482// StateYaledTimed(DataExpr)
4483template <atermpp::IsATerm Term>
4485{
4486#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4487 // check the type of the term
4488 const atermpp::aterm& term(t);
4489 if (!term.type_is_appl())
4490 {
4491 return false;
4492 }
4493 if (term.function() != core::detail::function_symbols::StateYaledTimed)
4494 {
4495 return false;
4496 }
4497
4498 // check the children
4499 if (term.size() != 1)
4500 {
4501 return false;
4502 }
4503#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4504 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4505 {
4506 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
4507 return false;
4508 }
4509#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4510
4511#endif // MCRL2_NO_SOUNDNESS_CHECKS
4512 return true;
4513}
4514
4515// StateDelay()
4516template <atermpp::IsATerm Term>
4518{
4519#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4520 // check the type of the term
4521 const atermpp::aterm& term(t);
4522 if (!term.type_is_appl())
4523 {
4524 return false;
4525 }
4526 if (term.function() != core::detail::function_symbols::StateDelay)
4527 {
4528 return false;
4529 }
4530
4531 // check the children
4532 if (term.size() != 0)
4533 {
4534 return false;
4535 }
4536
4537#endif // MCRL2_NO_SOUNDNESS_CHECKS
4538 return true;
4539}
4540
4541// StateDelayTimed(DataExpr)
4542template <atermpp::IsATerm Term>
4544{
4545#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4546 // check the type of the term
4547 const atermpp::aterm& term(t);
4548 if (!term.type_is_appl())
4549 {
4550 return false;
4551 }
4552 if (term.function() != core::detail::function_symbols::StateDelayTimed)
4553 {
4554 return false;
4555 }
4556
4557 // check the children
4558 if (term.size() != 1)
4559 {
4560 return false;
4561 }
4562#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4563 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4564 {
4565 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
4566 return false;
4567 }
4568#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4569
4570#endif // MCRL2_NO_SOUNDNESS_CHECKS
4571 return true;
4572}
4573
4574// StateVar(String, DataExpr*)
4575template <atermpp::IsATerm Term>
4576bool check_term_StateVar([[maybe_unused]] const Term& t)
4577{
4578#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4579 // check the type of the term
4580 const atermpp::aterm& term(t);
4581 if (!term.type_is_appl())
4582 {
4583 return false;
4584 }
4585 if (term.function() != core::detail::function_symbols::StateVar)
4586 {
4587 return false;
4588 }
4589
4590 // check the children
4591 if (term.size() != 2)
4592 {
4593 return false;
4594 }
4595#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4596 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4597 {
4598 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
4599 return false;
4600 }
4601 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
4602 {
4603 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
4604 return false;
4605 }
4606#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4607
4608#endif // MCRL2_NO_SOUNDNESS_CHECKS
4609 return true;
4610}
4611
4612// StateNu(String, DataVarIdInit*, StateFrm)
4613template <atermpp::IsATerm Term>
4614bool check_term_StateNu([[maybe_unused]] const Term& t)
4615{
4616#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4617 // check the type of the term
4618 const atermpp::aterm& term(t);
4619 if (!term.type_is_appl())
4620 {
4621 return false;
4622 }
4623 if (term.function() != core::detail::function_symbols::StateNu)
4624 {
4625 return false;
4626 }
4627
4628 // check the children
4629 if (term.size() != 3)
4630 {
4631 return false;
4632 }
4633#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4634 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4635 {
4636 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
4637 return false;
4638 }
4639 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
4640 {
4641 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarIdInit" << std::endl;
4642 return false;
4643 }
4644 if (!check_term_argument(term[2], check_rule_StateFrm<atermpp::aterm>))
4645 {
4646 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4647 return false;
4648 }
4649#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4650
4651#endif // MCRL2_NO_SOUNDNESS_CHECKS
4652 return true;
4653}
4654
4655// StateMu(String, DataVarIdInit*, StateFrm)
4656template <atermpp::IsATerm Term>
4657bool check_term_StateMu([[maybe_unused]] const Term& t)
4658{
4659#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4660 // check the type of the term
4661 const atermpp::aterm& term(t);
4662 if (!term.type_is_appl())
4663 {
4664 return false;
4665 }
4666 if (term.function() != core::detail::function_symbols::StateMu)
4667 {
4668 return false;
4669 }
4670
4671 // check the children
4672 if (term.size() != 3)
4673 {
4674 return false;
4675 }
4676#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4677 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4678 {
4679 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
4680 return false;
4681 }
4682 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
4683 {
4684 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarIdInit" << std::endl;
4685 return false;
4686 }
4687 if (!check_term_argument(term[2], check_rule_StateFrm<atermpp::aterm>))
4688 {
4689 mCRL2log(log::log_level_t::debug) << "check_rule_StateFrm" << std::endl;
4690 return false;
4691 }
4692#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4693
4694#endif // MCRL2_NO_SOUNDNESS_CHECKS
4695 return true;
4696}
4697
4698// RegNil()
4699template <atermpp::IsATerm Term>
4700bool check_term_RegNil([[maybe_unused]] const Term& t)
4701{
4702#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4703 // check the type of the term
4704 const atermpp::aterm& term(t);
4705 if (!term.type_is_appl())
4706 {
4707 return false;
4708 }
4709 if (term.function() != core::detail::function_symbols::RegNil)
4710 {
4711 return false;
4712 }
4713
4714 // check the children
4715 if (term.size() != 0)
4716 {
4717 return false;
4718 }
4719
4720#endif // MCRL2_NO_SOUNDNESS_CHECKS
4721 return true;
4722}
4723
4724// RegSeq(RegFrm, RegFrm)
4725template <atermpp::IsATerm Term>
4726bool check_term_RegSeq([[maybe_unused]] const Term& t)
4727{
4728#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4729 // check the type of the term
4730 const atermpp::aterm& term(t);
4731 if (!term.type_is_appl())
4732 {
4733 return false;
4734 }
4735 if (term.function() != core::detail::function_symbols::RegSeq)
4736 {
4737 return false;
4738 }
4739
4740 // check the children
4741 if (term.size() != 2)
4742 {
4743 return false;
4744 }
4745#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4746 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4747 {
4748 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4749 return false;
4750 }
4751 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4752 {
4753 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4754 return false;
4755 }
4756#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4757
4758#endif // MCRL2_NO_SOUNDNESS_CHECKS
4759 return true;
4760}
4761
4762// RegAlt(RegFrm, RegFrm)
4763template <atermpp::IsATerm Term>
4764bool check_term_RegAlt([[maybe_unused]] const Term& t)
4765{
4766#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4767 // check the type of the term
4768 const atermpp::aterm& term(t);
4769 if (!term.type_is_appl())
4770 {
4771 return false;
4772 }
4773 if (term.function() != core::detail::function_symbols::RegAlt)
4774 {
4775 return false;
4776 }
4777
4778 // check the children
4779 if (term.size() != 2)
4780 {
4781 return false;
4782 }
4783#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4784 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4785 {
4786 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4787 return false;
4788 }
4789 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4790 {
4791 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4792 return false;
4793 }
4794#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4795
4796#endif // MCRL2_NO_SOUNDNESS_CHECKS
4797 return true;
4798}
4799
4800// RegTrans(RegFrm)
4801template <atermpp::IsATerm Term>
4802bool check_term_RegTrans([[maybe_unused]] const Term& t)
4803{
4804#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4805 // check the type of the term
4806 const atermpp::aterm& term(t);
4807 if (!term.type_is_appl())
4808 {
4809 return false;
4810 }
4811 if (term.function() != core::detail::function_symbols::RegTrans)
4812 {
4813 return false;
4814 }
4815
4816 // check the children
4817 if (term.size() != 1)
4818 {
4819 return false;
4820 }
4821#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4822 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4823 {
4824 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4825 return false;
4826 }
4827#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4828
4829#endif // MCRL2_NO_SOUNDNESS_CHECKS
4830 return true;
4831}
4832
4833// RegTransOrNil(RegFrm)
4834template <atermpp::IsATerm Term>
4836{
4837#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4838 // check the type of the term
4839 const atermpp::aterm& term(t);
4840 if (!term.type_is_appl())
4841 {
4842 return false;
4843 }
4844 if (term.function() != core::detail::function_symbols::RegTransOrNil)
4845 {
4846 return false;
4847 }
4848
4849 // check the children
4850 if (term.size() != 1)
4851 {
4852 return false;
4853 }
4854#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4855 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4856 {
4857 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4858 return false;
4859 }
4860#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4861
4862#endif // MCRL2_NO_SOUNDNESS_CHECKS
4863 return true;
4864}
4865
4866// UntypedRegFrm(String, RegFrm, RegFrm)
4867template <atermpp::IsATerm Term>
4869{
4870#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4871 // check the type of the term
4872 const atermpp::aterm& term(t);
4873 if (!term.type_is_appl())
4874 {
4875 return false;
4876 }
4877 if (term.function() != core::detail::function_symbols::UntypedRegFrm)
4878 {
4879 return false;
4880 }
4881
4882 // check the children
4883 if (term.size() != 3)
4884 {
4885 return false;
4886 }
4887#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4888 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4889 {
4890 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
4891 return false;
4892 }
4893 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4894 {
4895 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4896 return false;
4897 }
4898 if (!check_term_argument(term[2], check_rule_RegFrm<atermpp::aterm>))
4899 {
4900 mCRL2log(log::log_level_t::debug) << "check_rule_RegFrm" << std::endl;
4901 return false;
4902 }
4903#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4904
4905#endif // MCRL2_NO_SOUNDNESS_CHECKS
4906 return true;
4907}
4908
4909// ActTrue()
4910template <atermpp::IsATerm Term>
4911bool check_term_ActTrue([[maybe_unused]] const Term& t)
4912{
4913#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4914 // check the type of the term
4915 const atermpp::aterm& term(t);
4916 if (!term.type_is_appl())
4917 {
4918 return false;
4919 }
4920 if (term.function() != core::detail::function_symbols::ActTrue)
4921 {
4922 return false;
4923 }
4924
4925 // check the children
4926 if (term.size() != 0)
4927 {
4928 return false;
4929 }
4930
4931#endif // MCRL2_NO_SOUNDNESS_CHECKS
4932 return true;
4933}
4934
4935// ActFalse()
4936template <atermpp::IsATerm Term>
4937bool check_term_ActFalse([[maybe_unused]] const Term& t)
4938{
4939#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4940 // check the type of the term
4941 const atermpp::aterm& term(t);
4942 if (!term.type_is_appl())
4943 {
4944 return false;
4945 }
4946 if (term.function() != core::detail::function_symbols::ActFalse)
4947 {
4948 return false;
4949 }
4950
4951 // check the children
4952 if (term.size() != 0)
4953 {
4954 return false;
4955 }
4956
4957#endif // MCRL2_NO_SOUNDNESS_CHECKS
4958 return true;
4959}
4960
4961// ActNot(ActFrm)
4962template <atermpp::IsATerm Term>
4963bool check_term_ActNot([[maybe_unused]] const Term& t)
4964{
4965#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4966 // check the type of the term
4967 const atermpp::aterm& term(t);
4968 if (!term.type_is_appl())
4969 {
4970 return false;
4971 }
4972 if (term.function() != core::detail::function_symbols::ActNot)
4973 {
4974 return false;
4975 }
4976
4977 // check the children
4978 if (term.size() != 1)
4979 {
4980 return false;
4981 }
4982#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4983 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
4984 {
4985 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
4986 return false;
4987 }
4988#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4989
4990#endif // MCRL2_NO_SOUNDNESS_CHECKS
4991 return true;
4992}
4993
4994// ActAnd(ActFrm, ActFrm)
4995template <atermpp::IsATerm Term>
4996bool check_term_ActAnd([[maybe_unused]] const Term& t)
4997{
4998#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4999 // check the type of the term
5000 const atermpp::aterm& term(t);
5001 if (!term.type_is_appl())
5002 {
5003 return false;
5004 }
5005 if (term.function() != core::detail::function_symbols::ActAnd)
5006 {
5007 return false;
5008 }
5009
5010 // check the children
5011 if (term.size() != 2)
5012 {
5013 return false;
5014 }
5015#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5016 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5017 {
5018 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5019 return false;
5020 }
5021 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5022 {
5023 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5024 return false;
5025 }
5026#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5027
5028#endif // MCRL2_NO_SOUNDNESS_CHECKS
5029 return true;
5030}
5031
5032// ActOr(ActFrm, ActFrm)
5033template <atermpp::IsATerm Term>
5034bool check_term_ActOr([[maybe_unused]] const Term& t)
5035{
5036#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5037 // check the type of the term
5038 const atermpp::aterm& term(t);
5039 if (!term.type_is_appl())
5040 {
5041 return false;
5042 }
5043 if (term.function() != core::detail::function_symbols::ActOr)
5044 {
5045 return false;
5046 }
5047
5048 // check the children
5049 if (term.size() != 2)
5050 {
5051 return false;
5052 }
5053#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5054 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5055 {
5056 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5057 return false;
5058 }
5059 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5060 {
5061 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5062 return false;
5063 }
5064#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5065
5066#endif // MCRL2_NO_SOUNDNESS_CHECKS
5067 return true;
5068}
5069
5070// ActImp(ActFrm, ActFrm)
5071template <atermpp::IsATerm Term>
5072bool check_term_ActImp([[maybe_unused]] const Term& t)
5073{
5074#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5075 // check the type of the term
5076 const atermpp::aterm& term(t);
5077 if (!term.type_is_appl())
5078 {
5079 return false;
5080 }
5081 if (term.function() != core::detail::function_symbols::ActImp)
5082 {
5083 return false;
5084 }
5085
5086 // check the children
5087 if (term.size() != 2)
5088 {
5089 return false;
5090 }
5091#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5092 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5093 {
5094 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5095 return false;
5096 }
5097 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5098 {
5099 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5100 return false;
5101 }
5102#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5103
5104#endif // MCRL2_NO_SOUNDNESS_CHECKS
5105 return true;
5106}
5107
5108// ActForall(DataVarId+, ActFrm)
5109template <atermpp::IsATerm Term>
5110bool check_term_ActForall([[maybe_unused]] const Term& t)
5111{
5112#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5113 // check the type of the term
5114 const atermpp::aterm& term(t);
5115 if (!term.type_is_appl())
5116 {
5117 return false;
5118 }
5119 if (term.function() != core::detail::function_symbols::ActForall)
5120 {
5121 return false;
5122 }
5123
5124 // check the children
5125 if (term.size() != 2)
5126 {
5127 return false;
5128 }
5129#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5130 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5131 {
5132 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
5133 return false;
5134 }
5135 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5136 {
5137 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5138 return false;
5139 }
5140#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5141
5142#endif // MCRL2_NO_SOUNDNESS_CHECKS
5143 return true;
5144}
5145
5146// ActExists(DataVarId+, ActFrm)
5147template <atermpp::IsATerm Term>
5148bool check_term_ActExists([[maybe_unused]] const Term& t)
5149{
5150#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5151 // check the type of the term
5152 const atermpp::aterm& term(t);
5153 if (!term.type_is_appl())
5154 {
5155 return false;
5156 }
5157 if (term.function() != core::detail::function_symbols::ActExists)
5158 {
5159 return false;
5160 }
5161
5162 // check the children
5163 if (term.size() != 2)
5164 {
5165 return false;
5166 }
5167#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5168 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5169 {
5170 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
5171 return false;
5172 }
5173 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5174 {
5175 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5176 return false;
5177 }
5178#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5179
5180#endif // MCRL2_NO_SOUNDNESS_CHECKS
5181 return true;
5182}
5183
5184// ActAt(ActFrm, DataExpr)
5185template <atermpp::IsATerm Term>
5186bool check_term_ActAt([[maybe_unused]] const Term& t)
5187{
5188#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5189 // check the type of the term
5190 const atermpp::aterm& term(t);
5191 if (!term.type_is_appl())
5192 {
5193 return false;
5194 }
5195 if (term.function() != core::detail::function_symbols::ActAt)
5196 {
5197 return false;
5198 }
5199
5200 // check the children
5201 if (term.size() != 2)
5202 {
5203 return false;
5204 }
5205#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5206 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5207 {
5208 mCRL2log(log::log_level_t::debug) << "check_rule_ActFrm" << std::endl;
5209 return false;
5210 }
5211 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
5212 {
5213 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
5214 return false;
5215 }
5216#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5217
5218#endif // MCRL2_NO_SOUNDNESS_CHECKS
5219 return true;
5220}
5221
5222// ActMultAct(Action*)
5223template <atermpp::IsATerm Term>
5225{
5226#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5227 // check the type of the term
5228 const atermpp::aterm& term(t);
5229 if (!term.type_is_appl())
5230 {
5231 return false;
5232 }
5233 if (term.function() != core::detail::function_symbols::ActMultAct)
5234 {
5235 return false;
5236 }
5237
5238 // check the children
5239 if (term.size() != 1)
5240 {
5241 return false;
5242 }
5243#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5244 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
5245 {
5246 mCRL2log(log::log_level_t::debug) << "check_rule_Action" << std::endl;
5247 return false;
5248 }
5249#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5250
5251#endif // MCRL2_NO_SOUNDNESS_CHECKS
5252 return true;
5253}
5254
5255// ActionRenameRules(ActionRenameRule*)
5256template <atermpp::IsATerm Term>
5258{
5259#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5260 // check the type of the term
5261 const atermpp::aterm& term(t);
5262 if (!term.type_is_appl())
5263 {
5264 return false;
5265 }
5266 if (term.function() != core::detail::function_symbols::ActionRenameRules)
5267 {
5268 return false;
5269 }
5270
5271 // check the children
5272 if (term.size() != 1)
5273 {
5274 return false;
5275 }
5276#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5277 if (!check_list_argument(term[0], check_rule_ActionRenameRule<atermpp::aterm>, 0))
5278 {
5279 mCRL2log(log::log_level_t::debug) << "check_rule_ActionRenameRule" << std::endl;
5280 return false;
5281 }
5282#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5283
5284#endif // MCRL2_NO_SOUNDNESS_CHECKS
5285 return true;
5286}
5287
5288// ActionRenameRule(DataVarId*, DataExpr, ParamIdOrAction, ActionRenameRuleRHS)
5289template <atermpp::IsATerm Term>
5291{
5292#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5293 // check the type of the term
5294 const atermpp::aterm& term(t);
5295 if (!term.type_is_appl())
5296 {
5297 return false;
5298 }
5299 if (term.function() != core::detail::function_symbols::ActionRenameRule)
5300 {
5301 return false;
5302 }
5303
5304 // check the children
5305 if (term.size() != 4)
5306 {
5307 return false;
5308 }
5309#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5310 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
5311 {
5312 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
5313 return false;
5314 }
5315 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
5316 {
5317 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
5318 return false;
5319 }
5320 if (!check_term_argument(term[2], check_rule_ParamIdOrAction<atermpp::aterm>))
5321 {
5322 mCRL2log(log::log_level_t::debug) << "check_rule_ParamIdOrAction" << std::endl;
5323 return false;
5324 }
5325 if (!check_term_argument(term[3], check_rule_ActionRenameRuleRHS<atermpp::aterm>))
5326 {
5327 mCRL2log(log::log_level_t::debug) << "check_rule_ActionRenameRuleRHS" << std::endl;
5328 return false;
5329 }
5330#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5331
5332#endif // MCRL2_NO_SOUNDNESS_CHECKS
5333 return true;
5334}
5335
5336// ActionRenameSpec(DataSpec, ActSpec, ActionRenameRules)
5337template <atermpp::IsATerm Term>
5339{
5340#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5341 // check the type of the term
5342 const atermpp::aterm& term(t);
5343 if (!term.type_is_appl())
5344 {
5345 return false;
5346 }
5347 if (term.function() != core::detail::function_symbols::ActionRenameSpec)
5348 {
5349 return false;
5350 }
5351
5352 // check the children
5353 if (term.size() != 3)
5354 {
5355 return false;
5356 }
5357#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5358 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
5359 {
5360 mCRL2log(log::log_level_t::debug) << "check_rule_DataSpec" << std::endl;
5361 return false;
5362 }
5363 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
5364 {
5365 mCRL2log(log::log_level_t::debug) << "check_rule_ActSpec" << std::endl;
5366 return false;
5367 }
5368 if (!check_term_argument(term[2], check_rule_ActionRenameRules<atermpp::aterm>))
5369 {
5370 mCRL2log(log::log_level_t::debug) << "check_rule_ActionRenameRules" << std::endl;
5371 return false;
5372 }
5373#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5374
5375#endif // MCRL2_NO_SOUNDNESS_CHECKS
5376 return true;
5377}
5378
5379// PBES(DataSpec, GlobVarSpec, PBEqnSpec, PBInit)
5380template <atermpp::IsATerm Term>
5381bool check_term_PBES([[maybe_unused]] const Term& t)
5382{
5383#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5384 // check the type of the term
5385 const atermpp::aterm& term(t);
5386 if (!term.type_is_appl())
5387 {
5388 return false;
5389 }
5390 if (term.function() != core::detail::function_symbols::PBES)
5391 {
5392 return false;
5393 }
5394
5395 // check the children
5396 if (term.size() != 4)
5397 {
5398 return false;
5399 }
5400#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5401 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
5402 {
5403 mCRL2log(log::log_level_t::debug) << "check_rule_DataSpec" << std::endl;
5404 return false;
5405 }
5406 if (!check_term_argument(term[1], check_rule_GlobVarSpec<atermpp::aterm>))
5407 {
5408 mCRL2log(log::log_level_t::debug) << "check_rule_GlobVarSpec" << std::endl;
5409 return false;
5410 }
5411 if (!check_term_argument(term[2], check_rule_PBEqnSpec<atermpp::aterm>))
5412 {
5413 mCRL2log(log::log_level_t::debug) << "check_rule_PBEqnSpec" << std::endl;
5414 return false;
5415 }
5416 if (!check_term_argument(term[3], check_rule_PBInit<atermpp::aterm>))
5417 {
5418 mCRL2log(log::log_level_t::debug) << "check_rule_PBInit" << std::endl;
5419 return false;
5420 }
5421#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5422
5423#endif // MCRL2_NO_SOUNDNESS_CHECKS
5424 return true;
5425}
5426
5427// PBEqnSpec(PBEqn*)
5428template <atermpp::IsATerm Term>
5429bool check_term_PBEqnSpec([[maybe_unused]] const Term& t)
5430{
5431#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5432 // check the type of the term
5433 const atermpp::aterm& term(t);
5434 if (!term.type_is_appl())
5435 {
5436 return false;
5437 }
5438 if (term.function() != core::detail::function_symbols::PBEqnSpec)
5439 {
5440 return false;
5441 }
5442
5443 // check the children
5444 if (term.size() != 1)
5445 {
5446 return false;
5447 }
5448#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5449 if (!check_list_argument(term[0], check_rule_PBEqn<atermpp::aterm>, 0))
5450 {
5451 mCRL2log(log::log_level_t::debug) << "check_rule_PBEqn" << std::endl;
5452 return false;
5453 }
5454#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5455
5456#endif // MCRL2_NO_SOUNDNESS_CHECKS
5457 return true;
5458}
5459
5460// PBInit(PropVarInst)
5461template <atermpp::IsATerm Term>
5462bool check_term_PBInit([[maybe_unused]] const Term& t)
5463{
5464#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5465 // check the type of the term
5466 const atermpp::aterm& term(t);
5467 if (!term.type_is_appl())
5468 {
5469 return false;
5470 }
5471 if (term.function() != core::detail::function_symbols::PBInit)
5472 {
5473 return false;
5474 }
5475
5476 // check the children
5477 if (term.size() != 1)
5478 {
5479 return false;
5480 }
5481#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5482 if (!check_term_argument(term[0], check_rule_PropVarInst<atermpp::aterm>))
5483 {
5484 mCRL2log(log::log_level_t::debug) << "check_rule_PropVarInst" << std::endl;
5485 return false;
5486 }
5487#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5488
5489#endif // MCRL2_NO_SOUNDNESS_CHECKS
5490 return true;
5491}
5492
5493// PBEqn(FixPoint, PropVarDecl, PBExpr)
5494template <atermpp::IsATerm Term>
5495bool check_term_PBEqn([[maybe_unused]] const Term& t)
5496{
5497#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5498 // check the type of the term
5499 const atermpp::aterm& term(t);
5500 if (!term.type_is_appl())
5501 {
5502 return false;
5503 }
5504 if (term.function() != core::detail::function_symbols::PBEqn)
5505 {
5506 return false;
5507 }
5508
5509 // check the children
5510 if (term.size() != 3)
5511 {
5512 return false;
5513 }
5514#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5515 if (!check_term_argument(term[0], check_rule_FixPoint<atermpp::aterm>))
5516 {
5517 mCRL2log(log::log_level_t::debug) << "check_rule_FixPoint" << std::endl;
5518 return false;
5519 }
5520 if (!check_term_argument(term[1], check_rule_PropVarDecl<atermpp::aterm>))
5521 {
5522 mCRL2log(log::log_level_t::debug) << "check_rule_PropVarDecl" << std::endl;
5523 return false;
5524 }
5525 if (!check_term_argument(term[2], check_rule_PBExpr<atermpp::aterm>))
5526 {
5527 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5528 return false;
5529 }
5530#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5531
5532#endif // MCRL2_NO_SOUNDNESS_CHECKS
5533 return true;
5534}
5535
5536// Mu()
5537template <atermpp::IsATerm Term>
5538bool check_term_Mu([[maybe_unused]] const Term& t)
5539{
5540#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5541 // check the type of the term
5542 const atermpp::aterm& term(t);
5543 if (!term.type_is_appl())
5544 {
5545 return false;
5546 }
5547 if (term.function() != core::detail::function_symbols::Mu)
5548 {
5549 return false;
5550 }
5551
5552 // check the children
5553 if (term.size() != 0)
5554 {
5555 return false;
5556 }
5557
5558#endif // MCRL2_NO_SOUNDNESS_CHECKS
5559 return true;
5560}
5561
5562// Nu()
5563template <atermpp::IsATerm Term>
5564bool check_term_Nu([[maybe_unused]] const Term& t)
5565{
5566#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5567 // check the type of the term
5568 const atermpp::aterm& term(t);
5569 if (!term.type_is_appl())
5570 {
5571 return false;
5572 }
5573 if (term.function() != core::detail::function_symbols::Nu)
5574 {
5575 return false;
5576 }
5577
5578 // check the children
5579 if (term.size() != 0)
5580 {
5581 return false;
5582 }
5583
5584#endif // MCRL2_NO_SOUNDNESS_CHECKS
5585 return true;
5586}
5587
5588// PropVarDecl(String, DataVarId*)
5589template <atermpp::IsATerm Term>
5591{
5592#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5593 // check the type of the term
5594 const atermpp::aterm& term(t);
5595 if (!term.type_is_appl())
5596 {
5597 return false;
5598 }
5599 if (term.function() != core::detail::function_symbols::PropVarDecl)
5600 {
5601 return false;
5602 }
5603
5604 // check the children
5605 if (term.size() != 2)
5606 {
5607 return false;
5608 }
5609#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5610 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
5611 {
5612 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
5613 return false;
5614 }
5615 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
5616 {
5617 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
5618 return false;
5619 }
5620#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5621
5622#endif // MCRL2_NO_SOUNDNESS_CHECKS
5623 return true;
5624}
5625
5626// PBESTrue()
5627template <atermpp::IsATerm Term>
5628bool check_term_PBESTrue([[maybe_unused]] const Term& t)
5629{
5630#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5631 // check the type of the term
5632 const atermpp::aterm& term(t);
5633 if (!term.type_is_appl())
5634 {
5635 return false;
5636 }
5637 if (term.function() != core::detail::function_symbols::PBESTrue)
5638 {
5639 return false;
5640 }
5641
5642 // check the children
5643 if (term.size() != 0)
5644 {
5645 return false;
5646 }
5647
5648#endif // MCRL2_NO_SOUNDNESS_CHECKS
5649 return true;
5650}
5651
5652// PBESFalse()
5653template <atermpp::IsATerm Term>
5654bool check_term_PBESFalse([[maybe_unused]] const Term& t)
5655{
5656#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5657 // check the type of the term
5658 const atermpp::aterm& term(t);
5659 if (!term.type_is_appl())
5660 {
5661 return false;
5662 }
5663 if (term.function() != core::detail::function_symbols::PBESFalse)
5664 {
5665 return false;
5666 }
5667
5668 // check the children
5669 if (term.size() != 0)
5670 {
5671 return false;
5672 }
5673
5674#endif // MCRL2_NO_SOUNDNESS_CHECKS
5675 return true;
5676}
5677
5678// PBESNot(PBExpr)
5679template <atermpp::IsATerm Term>
5680bool check_term_PBESNot([[maybe_unused]] const Term& t)
5681{
5682#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5683 // check the type of the term
5684 const atermpp::aterm& term(t);
5685 if (!term.type_is_appl())
5686 {
5687 return false;
5688 }
5689 if (term.function() != core::detail::function_symbols::PBESNot)
5690 {
5691 return false;
5692 }
5693
5694 // check the children
5695 if (term.size() != 1)
5696 {
5697 return false;
5698 }
5699#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5700 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5701 {
5702 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5703 return false;
5704 }
5705#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5706
5707#endif // MCRL2_NO_SOUNDNESS_CHECKS
5708 return true;
5709}
5710
5711// PBESAnd(PBExpr, PBExpr)
5712template <atermpp::IsATerm Term>
5713bool check_term_PBESAnd([[maybe_unused]] const Term& t)
5714{
5715#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5716 // check the type of the term
5717 const atermpp::aterm& term(t);
5718 if (!term.type_is_appl())
5719 {
5720 return false;
5721 }
5722 if (term.function() != core::detail::function_symbols::PBESAnd)
5723 {
5724 return false;
5725 }
5726
5727 // check the children
5728 if (term.size() != 2)
5729 {
5730 return false;
5731 }
5732#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5733 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5734 {
5735 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5736 return false;
5737 }
5738 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5739 {
5740 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5741 return false;
5742 }
5743#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5744
5745#endif // MCRL2_NO_SOUNDNESS_CHECKS
5746 return true;
5747}
5748
5749// PBESOr(PBExpr, PBExpr)
5750template <atermpp::IsATerm Term>
5751bool check_term_PBESOr([[maybe_unused]] const Term& t)
5752{
5753#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5754 // check the type of the term
5755 const atermpp::aterm& term(t);
5756 if (!term.type_is_appl())
5757 {
5758 return false;
5759 }
5760 if (term.function() != core::detail::function_symbols::PBESOr)
5761 {
5762 return false;
5763 }
5764
5765 // check the children
5766 if (term.size() != 2)
5767 {
5768 return false;
5769 }
5770#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5771 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5772 {
5773 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5774 return false;
5775 }
5776 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5777 {
5778 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5779 return false;
5780 }
5781#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5782
5783#endif // MCRL2_NO_SOUNDNESS_CHECKS
5784 return true;
5785}
5786
5787// PBESImp(PBExpr, PBExpr)
5788template <atermpp::IsATerm Term>
5789bool check_term_PBESImp([[maybe_unused]] const Term& t)
5790{
5791#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5792 // check the type of the term
5793 const atermpp::aterm& term(t);
5794 if (!term.type_is_appl())
5795 {
5796 return false;
5797 }
5798 if (term.function() != core::detail::function_symbols::PBESImp)
5799 {
5800 return false;
5801 }
5802
5803 // check the children
5804 if (term.size() != 2)
5805 {
5806 return false;
5807 }
5808#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5809 if (!check_term_argument(term[0], check_rule_PBExpr<atermpp::aterm>))
5810 {
5811 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5812 return false;
5813 }
5814 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5815 {
5816 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5817 return false;
5818 }
5819#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5820
5821#endif // MCRL2_NO_SOUNDNESS_CHECKS
5822 return true;
5823}
5824
5825// PBESForall(DataVarId+, PBExpr)
5826template <atermpp::IsATerm Term>
5828{
5829#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5830 // check the type of the term
5831 const atermpp::aterm& term(t);
5832 if (!term.type_is_appl())
5833 {
5834 return false;
5835 }
5836 if (term.function() != core::detail::function_symbols::PBESForall)
5837 {
5838 return false;
5839 }
5840
5841 // check the children
5842 if (term.size() != 2)
5843 {
5844 return false;
5845 }
5846#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5847 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5848 {
5849 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
5850 return false;
5851 }
5852 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5853 {
5854 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5855 return false;
5856 }
5857#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5858
5859#endif // MCRL2_NO_SOUNDNESS_CHECKS
5860 return true;
5861}
5862
5863// PBESExists(DataVarId+, PBExpr)
5864template <atermpp::IsATerm Term>
5866{
5867#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5868 // check the type of the term
5869 const atermpp::aterm& term(t);
5870 if (!term.type_is_appl())
5871 {
5872 return false;
5873 }
5874 if (term.function() != core::detail::function_symbols::PBESExists)
5875 {
5876 return false;
5877 }
5878
5879 // check the children
5880 if (term.size() != 2)
5881 {
5882 return false;
5883 }
5884#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5885 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5886 {
5887 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
5888 return false;
5889 }
5890 if (!check_term_argument(term[1], check_rule_PBExpr<atermpp::aterm>))
5891 {
5892 mCRL2log(log::log_level_t::debug) << "check_rule_PBExpr" << std::endl;
5893 return false;
5894 }
5895#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5896
5897#endif // MCRL2_NO_SOUNDNESS_CHECKS
5898 return true;
5899}
5900
5901// PropVarInst(String, DataExpr*)
5902template <atermpp::IsATerm Term>
5904{
5905#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5906 // check the type of the term
5907 const atermpp::aterm& term(t);
5908 if (!term.type_is_appl())
5909 {
5910 return false;
5911 }
5912 if (term.function() != core::detail::function_symbols::PropVarInst)
5913 {
5914 return false;
5915 }
5916
5917 // check the children
5918 if (term.size() != 2)
5919 {
5920 return false;
5921 }
5922#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5923 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
5924 {
5925 mCRL2log(log::log_level_t::debug) << "check_rule_String" << std::endl;
5926 return false;
5927 }
5928 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
5929 {
5930 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
5931 return false;
5932 }
5933#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5934
5935#endif // MCRL2_NO_SOUNDNESS_CHECKS
5936 return true;
5937}
5938
5939// PRES(DataSpec, GlobVarSpec, PREqnSpec, PRInit)
5940template <atermpp::IsATerm Term>
5941bool check_term_PRES([[maybe_unused]] const Term& t)
5942{
5943#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5944 // check the type of the term
5945 const atermpp::aterm& term(t);
5946 if (!term.type_is_appl())
5947 {
5948 return false;
5949 }
5950 if (term.function() != core::detail::function_symbols::PRES)
5951 {
5952 return false;
5953 }
5954
5955 // check the children
5956 if (term.size() != 4)
5957 {
5958 return false;
5959 }
5960#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5961 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
5962 {
5963 mCRL2log(log::log_level_t::debug) << "check_rule_DataSpec" << std::endl;
5964 return false;
5965 }
5966 if (!check_term_argument(term[1], check_rule_GlobVarSpec<atermpp::aterm>))
5967 {
5968 mCRL2log(log::log_level_t::debug) << "check_rule_GlobVarSpec" << std::endl;
5969 return false;
5970 }
5971 if (!check_term_argument(term[2], check_rule_PREqnSpec<atermpp::aterm>))
5972 {
5973 mCRL2log(log::log_level_t::debug) << "check_rule_PREqnSpec" << std::endl;
5974 return false;
5975 }
5976 if (!check_term_argument(term[3], check_rule_PRInit<atermpp::aterm>))
5977 {
5978 mCRL2log(log::log_level_t::debug) << "check_rule_PRInit" << std::endl;
5979 return false;
5980 }
5981#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5982
5983#endif // MCRL2_NO_SOUNDNESS_CHECKS
5984 return true;
5985}
5986
5987// PREqnSpec(PREqn*)
5988template <atermpp::IsATerm Term>
5989bool check_term_PREqnSpec([[maybe_unused]] const Term& t)
5990{
5991#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5992 // check the type of the term
5993 const atermpp::aterm& term(t);
5994 if (!term.type_is_appl())
5995 {
5996 return false;
5997 }
5998 if (term.function() != core::detail::function_symbols::PREqnSpec)
5999 {
6000 return false;
6001 }
6002
6003 // check the children
6004 if (term.size() != 1)
6005 {
6006 return false;
6007 }
6008#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6009 if (!check_list_argument(term[0], check_rule_PREqn<atermpp::aterm>, 0))
6010 {
6011 mCRL2log(log::log_level_t::debug) << "check_rule_PREqn" << std::endl;
6012 return false;
6013 }
6014#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6015
6016#endif // MCRL2_NO_SOUNDNESS_CHECKS
6017 return true;
6018}
6019
6020// PRInit(PropVarInst)
6021template <atermpp::IsATerm Term>
6022bool check_term_PRInit([[maybe_unused]] const Term& t)
6023{
6024#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6025 // check the type of the term
6026 const atermpp::aterm& term(t);
6027 if (!term.type_is_appl())
6028 {
6029 return false;
6030 }
6031 if (term.function() != core::detail::function_symbols::PRInit)
6032 {
6033 return false;
6034 }
6035
6036 // check the children
6037 if (term.size() != 1)
6038 {
6039 return false;
6040 }
6041#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6042 if (!check_term_argument(term[0], check_rule_PropVarInst<atermpp::aterm>))
6043 {
6044 mCRL2log(log::log_level_t::debug) << "check_rule_PropVarInst" << std::endl;
6045 return false;
6046 }
6047#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6048
6049#endif // MCRL2_NO_SOUNDNESS_CHECKS
6050 return true;
6051}
6052
6053// PREqn(FixPoint, PropVarDecl, PRExpr)
6054template <atermpp::IsATerm Term>
6055bool check_term_PREqn([[maybe_unused]] const Term& t)
6056{
6057#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6058 // check the type of the term
6059 const atermpp::aterm& term(t);
6060 if (!term.type_is_appl())
6061 {
6062 return false;
6063 }
6064 if (term.function() != core::detail::function_symbols::PREqn)
6065 {
6066 return false;
6067 }
6068
6069 // check the children
6070 if (term.size() != 3)
6071 {
6072 return false;
6073 }
6074#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6075 if (!check_term_argument(term[0], check_rule_FixPoint<atermpp::aterm>))
6076 {
6077 mCRL2log(log::log_level_t::debug) << "check_rule_FixPoint" << std::endl;
6078 return false;
6079 }
6080 if (!check_term_argument(term[1], check_rule_PropVarDecl<atermpp::aterm>))
6081 {
6082 mCRL2log(log::log_level_t::debug) << "check_rule_PropVarDecl" << std::endl;
6083 return false;
6084 }
6085 if (!check_term_argument(term[2], check_rule_PRExpr<atermpp::aterm>))
6086 {
6087 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6088 return false;
6089 }
6090#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6091
6092#endif // MCRL2_NO_SOUNDNESS_CHECKS
6093 return true;
6094}
6095
6096// PRESTrue()
6097template <atermpp::IsATerm Term>
6098bool check_term_PRESTrue([[maybe_unused]] const Term& t)
6099{
6100#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6101 // check the type of the term
6102 const atermpp::aterm& term(t);
6103 if (!term.type_is_appl())
6104 {
6105 return false;
6106 }
6107 if (term.function() != core::detail::function_symbols::PRESTrue)
6108 {
6109 return false;
6110 }
6111
6112 // check the children
6113 if (term.size() != 0)
6114 {
6115 return false;
6116 }
6117
6118#endif // MCRL2_NO_SOUNDNESS_CHECKS
6119 return true;
6120}
6121
6122// PRESFalse()
6123template <atermpp::IsATerm Term>
6124bool check_term_PRESFalse([[maybe_unused]] const Term& t)
6125{
6126#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6127 // check the type of the term
6128 const atermpp::aterm& term(t);
6129 if (!term.type_is_appl())
6130 {
6131 return false;
6132 }
6133 if (term.function() != core::detail::function_symbols::PRESFalse)
6134 {
6135 return false;
6136 }
6137
6138 // check the children
6139 if (term.size() != 0)
6140 {
6141 return false;
6142 }
6143
6144#endif // MCRL2_NO_SOUNDNESS_CHECKS
6145 return true;
6146}
6147
6148// PRESMinus(PRExpr)
6149template <atermpp::IsATerm Term>
6150bool check_term_PRESMinus([[maybe_unused]] const Term& t)
6151{
6152#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6153 // check the type of the term
6154 const atermpp::aterm& term(t);
6155 if (!term.type_is_appl())
6156 {
6157 return false;
6158 }
6159 if (term.function() != core::detail::function_symbols::PRESMinus)
6160 {
6161 return false;
6162 }
6163
6164 // check the children
6165 if (term.size() != 1)
6166 {
6167 return false;
6168 }
6169#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6170 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6171 {
6172 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6173 return false;
6174 }
6175#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6176
6177#endif // MCRL2_NO_SOUNDNESS_CHECKS
6178 return true;
6179}
6180
6181// PRESAnd(PRExpr, PRExpr)
6182template <atermpp::IsATerm Term>
6183bool check_term_PRESAnd([[maybe_unused]] const Term& t)
6184{
6185#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6186 // check the type of the term
6187 const atermpp::aterm& term(t);
6188 if (!term.type_is_appl())
6189 {
6190 return false;
6191 }
6192 if (term.function() != core::detail::function_symbols::PRESAnd)
6193 {
6194 return false;
6195 }
6196
6197 // check the children
6198 if (term.size() != 2)
6199 {
6200 return false;
6201 }
6202#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6203 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6204 {
6205 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6206 return false;
6207 }
6208 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6209 {
6210 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6211 return false;
6212 }
6213#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6214
6215#endif // MCRL2_NO_SOUNDNESS_CHECKS
6216 return true;
6217}
6218
6219// PRESOr(PRExpr, PRExpr)
6220template <atermpp::IsATerm Term>
6221bool check_term_PRESOr([[maybe_unused]] const Term& t)
6222{
6223#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6224 // check the type of the term
6225 const atermpp::aterm& term(t);
6226 if (!term.type_is_appl())
6227 {
6228 return false;
6229 }
6230 if (term.function() != core::detail::function_symbols::PRESOr)
6231 {
6232 return false;
6233 }
6234
6235 // check the children
6236 if (term.size() != 2)
6237 {
6238 return false;
6239 }
6240#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6241 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6242 {
6243 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6244 return false;
6245 }
6246 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6247 {
6248 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6249 return false;
6250 }
6251#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6252
6253#endif // MCRL2_NO_SOUNDNESS_CHECKS
6254 return true;
6255}
6256
6257// PRESImp(PRExpr, PRExpr)
6258template <atermpp::IsATerm Term>
6259bool check_term_PRESImp([[maybe_unused]] const Term& t)
6260{
6261#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6262 // check the type of the term
6263 const atermpp::aterm& term(t);
6264 if (!term.type_is_appl())
6265 {
6266 return false;
6267 }
6268 if (term.function() != core::detail::function_symbols::PRESImp)
6269 {
6270 return false;
6271 }
6272
6273 // check the children
6274 if (term.size() != 2)
6275 {
6276 return false;
6277 }
6278#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6279 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6280 {
6281 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6282 return false;
6283 }
6284 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6285 {
6286 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6287 return false;
6288 }
6289#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6290
6291#endif // MCRL2_NO_SOUNDNESS_CHECKS
6292 return true;
6293}
6294
6295// PRESPlus(PRExpr, PRExpr)
6296template <atermpp::IsATerm Term>
6297bool check_term_PRESPlus([[maybe_unused]] const Term& t)
6298{
6299#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6300 // check the type of the term
6301 const atermpp::aterm& term(t);
6302 if (!term.type_is_appl())
6303 {
6304 return false;
6305 }
6306 if (term.function() != core::detail::function_symbols::PRESPlus)
6307 {
6308 return false;
6309 }
6310
6311 // check the children
6312 if (term.size() != 2)
6313 {
6314 return false;
6315 }
6316#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6317 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6318 {
6319 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6320 return false;
6321 }
6322 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6323 {
6324 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6325 return false;
6326 }
6327#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6328
6329#endif // MCRL2_NO_SOUNDNESS_CHECKS
6330 return true;
6331}
6332
6333// PRESConstantMultiply(DataExpr, PRExpr)
6334template <atermpp::IsATerm Term>
6336{
6337#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6338 // check the type of the term
6339 const atermpp::aterm& term(t);
6340 if (!term.type_is_appl())
6341 {
6342 return false;
6343 }
6344 if (term.function() != core::detail::function_symbols::PRESConstantMultiply)
6345 {
6346 return false;
6347 }
6348
6349 // check the children
6350 if (term.size() != 2)
6351 {
6352 return false;
6353 }
6354#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6355 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
6356 {
6357 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
6358 return false;
6359 }
6360 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6361 {
6362 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6363 return false;
6364 }
6365#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6366
6367#endif // MCRL2_NO_SOUNDNESS_CHECKS
6368 return true;
6369}
6370
6371// PRESConstantMultiplyAlt(PRExpr, DataExpr)
6372template <atermpp::IsATerm Term>
6374{
6375#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6376 // check the type of the term
6377 const atermpp::aterm& term(t);
6378 if (!term.type_is_appl())
6379 {
6380 return false;
6381 }
6382 if (term.function() != core::detail::function_symbols::PRESConstantMultiplyAlt)
6383 {
6384 return false;
6385 }
6386
6387 // check the children
6388 if (term.size() != 2)
6389 {
6390 return false;
6391 }
6392#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6393 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6394 {
6395 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6396 return false;
6397 }
6398 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
6399 {
6400 mCRL2log(log::log_level_t::debug) << "check_rule_DataExpr" << std::endl;
6401 return false;
6402 }
6403#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6404
6405#endif // MCRL2_NO_SOUNDNESS_CHECKS
6406 return true;
6407}
6408
6409// PRESInfimum(DataVarId+, PRExpr)
6410template <atermpp::IsATerm Term>
6412{
6413#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6414 // check the type of the term
6415 const atermpp::aterm& term(t);
6416 if (!term.type_is_appl())
6417 {
6418 return false;
6419 }
6420 if (term.function() != core::detail::function_symbols::PRESInfimum)
6421 {
6422 return false;
6423 }
6424
6425 // check the children
6426 if (term.size() != 2)
6427 {
6428 return false;
6429 }
6430#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6431 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
6432 {
6433 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
6434 return false;
6435 }
6436 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6437 {
6438 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6439 return false;
6440 }
6441#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6442
6443#endif // MCRL2_NO_SOUNDNESS_CHECKS
6444 return true;
6445}
6446
6447// PRESSupremum(DataVarId+, PRExpr)
6448template <atermpp::IsATerm Term>
6450{
6451#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6452 // check the type of the term
6453 const atermpp::aterm& term(t);
6454 if (!term.type_is_appl())
6455 {
6456 return false;
6457 }
6458 if (term.function() != core::detail::function_symbols::PRESSupremum)
6459 {
6460 return false;
6461 }
6462
6463 // check the children
6464 if (term.size() != 2)
6465 {
6466 return false;
6467 }
6468#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6469 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
6470 {
6471 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
6472 return false;
6473 }
6474 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6475 {
6476 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6477 return false;
6478 }
6479#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6480
6481#endif // MCRL2_NO_SOUNDNESS_CHECKS
6482 return true;
6483}
6484
6485// PRESSum(DataVarId+, PRExpr)
6486template <atermpp::IsATerm Term>
6487bool check_term_PRESSum([[maybe_unused]] const Term& t)
6488{
6489#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6490 // check the type of the term
6491 const atermpp::aterm& term(t);
6492 if (!term.type_is_appl())
6493 {
6494 return false;
6495 }
6496 if (term.function() != core::detail::function_symbols::PRESSum)
6497 {
6498 return false;
6499 }
6500
6501 // check the children
6502 if (term.size() != 2)
6503 {
6504 return false;
6505 }
6506#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6507 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
6508 {
6509 mCRL2log(log::log_level_t::debug) << "check_rule_DataVarId" << std::endl;
6510 return false;
6511 }
6512 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6513 {
6514 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6515 return false;
6516 }
6517#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6518
6519#endif // MCRL2_NO_SOUNDNESS_CHECKS
6520 return true;
6521}
6522
6523// PRESEqInf(PRExpr)
6524template <atermpp::IsATerm Term>
6525bool check_term_PRESEqInf([[maybe_unused]] const Term& t)
6526{
6527#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6528 // check the type of the term
6529 const atermpp::aterm& term(t);
6530 if (!term.type_is_appl())
6531 {
6532 return false;
6533 }
6534 if (term.function() != core::detail::function_symbols::PRESEqInf)
6535 {
6536 return false;
6537 }
6538
6539 // check the children
6540 if (term.size() != 1)
6541 {
6542 return false;
6543 }
6544#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6545 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6546 {
6547 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6548 return false;
6549 }
6550#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6551
6552#endif // MCRL2_NO_SOUNDNESS_CHECKS
6553 return true;
6554}
6555
6556// PRESEqNInf(PRExpr)
6557template <atermpp::IsATerm Term>
6559{
6560#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6561 // check the type of the term
6562 const atermpp::aterm& term(t);
6563 if (!term.type_is_appl())
6564 {
6565 return false;
6566 }
6567 if (term.function() != core::detail::function_symbols::PRESEqNInf)
6568 {
6569 return false;
6570 }
6571
6572 // check the children
6573 if (term.size() != 1)
6574 {
6575 return false;
6576 }
6577#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6578 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6579 {
6580 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6581 return false;
6582 }
6583#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6584
6585#endif // MCRL2_NO_SOUNDNESS_CHECKS
6586 return true;
6587}
6588
6589// PRESCondSm(PRExpr, PRExpr, PRExpr)
6590template <atermpp::IsATerm Term>
6592{
6593#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6594 // check the type of the term
6595 const atermpp::aterm& term(t);
6596 if (!term.type_is_appl())
6597 {
6598 return false;
6599 }
6600 if (term.function() != core::detail::function_symbols::PRESCondSm)
6601 {
6602 return false;
6603 }
6604
6605 // check the children
6606 if (term.size() != 3)
6607 {
6608 return false;
6609 }
6610#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6611 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6612 {
6613 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6614 return false;
6615 }
6616 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6617 {
6618 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6619 return false;
6620 }
6621 if (!check_term_argument(term[2], check_rule_PRExpr<atermpp::aterm>))
6622 {
6623 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6624 return false;
6625 }
6626#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6627
6628#endif // MCRL2_NO_SOUNDNESS_CHECKS
6629 return true;
6630}
6631
6632// PRESCondEq(PRExpr, PRExpr, PRExpr)
6633template <atermpp::IsATerm Term>
6635{
6636#ifndef MCRL2_NO_SOUNDNESS_CHECKS
6637 // check the type of the term
6638 const atermpp::aterm& term(t);
6639 if (!term.type_is_appl())
6640 {
6641 return false;
6642 }
6643 if (term.function() != core::detail::function_symbols::PRESCondEq)
6644 {
6645 return false;
6646 }
6647
6648 // check the children
6649 if (term.size() != 3)
6650 {
6651 return false;
6652 }
6653#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6654 if (!check_term_argument(term[0], check_rule_PRExpr<atermpp::aterm>))
6655 {
6656 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6657 return false;
6658 }
6659 if (!check_term_argument(term[1], check_rule_PRExpr<atermpp::aterm>))
6660 {
6661 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6662 return false;
6663 }
6664 if (!check_term_argument(term[2], check_rule_PRExpr<atermpp::aterm>))
6665 {
6666 mCRL2log(log::log_level_t::debug) << "check_rule_PRExpr" << std::endl;
6667 return false;
6668 }
6669#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
6670
6671#endif // MCRL2_NO_SOUNDNESS_CHECKS
6672 return true;
6673}
6674//--- end generated code ---//
6675
6676} // namespace mcrl2::core::detail
6677
6678#endif // MCRL2_CORE_DETAIL_SOUNDNESS_CHECKS_H
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A list of aterm objects.
Definition aterm_list.h:26
A unordered_map class in which aterms can be stored.
apply_builder_arg1(const Arg1 &arg1)
Definition builder.h:120
apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:144
update_apply_builder_arg1(const Function &f, const Arg1 &arg1)
Definition builder.h:212
void apply(T &result, const argument_type &x)
Definition builder.h:207
An abstraction expression.
Definition abstraction.h:23
const variable_list & variables() const
Definition abstraction.h:60
const data_expression & body() const
Definition abstraction.h:65
\brief A sort alias
Definition alias.h:23
alias()
\brief Default constructor X3.
Definition alias.h:26
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.
Definition alias.h:39
alias(alias &&) noexcept=default
alias(const atermpp::aterm &term)
Definition alias.h:32
alias & operator=(alias &&) noexcept=default
const basic_sort & name() const
Definition alias.h:49
const sort_expression & reference() const
Definition alias.h:54
\brief Assignment expression
Definition assignment.h:24
\brief Assignment of a data expression to a variable
Definition assignment.h:88
const data_expression & rhs() const
Definition assignment.h:119
const variable & lhs() const
Definition assignment.h:114
universal quantification.
\brief A basic sort
Definition basic_sort.h:25
basic_sort(const basic_sort &) noexcept=default
Move semantics.
basic_sort()
\brief Default constructor X3.
Definition basic_sort.h:28
basic_sort & operator=(const basic_sort &) noexcept=default
const core::identifier_string & name() const
Definition basic_sort.h:56
basic_sort(basic_sort &&) noexcept=default
basic_sort(const core::identifier_string &name)
\brief Constructor Z14.
Definition basic_sort.h:41
basic_sort(const std::string &name)
\brief Constructor Z2.
Definition basic_sort.h:46
basic_sort & operator=(basic_sort &&) noexcept=default
basic_sort(const atermpp::aterm &term)
Definition basic_sort.h:34
\brief A container sort
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)
\brief A data equation
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.
Definition data.cpp:107
existential quantification.
Definition exists.h:23
universal quantification.
Definition forall.h:25
\brief A function sort
const sort_expression & codomain() const
const sort_expression_list & domain() const
\brief A function symbol
const core::identifier_string & name() const
const sort_expression & sort() const
function symbol.
Definition lambda.h:24
\brief A machine number
universal quantification.
\brief A sort expression
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
\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
const core::identifier_string & name() const
const data_expression_list & arguments() const
\brief Assignment of a data expression to a string
Definition assignment.h:179
const core::identifier_string & lhs() const
Definition assignment.h:210
const data_expression & rhs() const
Definition assignment.h:215
\brief An untyped identifier
const sort_expression_list & sorts() const
\brief Unknown sort expression
untyped_sort()
\brief Default constructor X3.
\brief A data variable
Definition variable.h:25
const core::identifier_string & name() const
Definition variable.h:35
const sort_expression & sort() const
Definition variable.h:40
\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.
Definition logger.h:435
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()
Definition builder.h:103
update_apply_builder_arg1< Builder, Function, Arg1 > make_update_apply_builder_arg1(const Function &f)
Definition builder.h:220
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)
Definition builder.h:127
update_apply_builder< Builder, Function > make_update_apply_builder(const Function &f)
Definition builder.h:186
apply_builder_arg2< Builder, Arg1, Arg2 > make_apply_builder_arg2(const Arg1 &arg1, const Arg2 &arg2)
Definition builder.h:151
data_expression parse_data_expression(const std::string &text)
Definition data.cpp:217
data_specification parse_data_specification_new(const std::string &text)
Definition data.cpp:228
variable_list parse_variable_declaration_list(const std::string &text)
Definition data.cpp:239
variable_list parse_variables(const std::string &text)
Definition data.cpp:206
sort_expression parse_sort_expression(const std::string &text)
Definition data.cpp:196
Namespace for system defined sort bool_.
Definition bool.h:29
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:41
std::string pp(const data::structured_sort_constructor_argument &x, bool arg0)
Definition data.cpp:71
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
Definition data.cpp:82
void normalize_sorts(data::data_equation_vector &x, const data::sort_specification &sortspec)
Definition data.cpp:84
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)
Definition data.cpp:83
std::string pp(const data::exists &x, bool arg0)
Definition data.cpp:53
std::string pp(const data::untyped_identifier_assignment &x, bool arg0)
Definition data.cpp:74
std::ostream & operator<<(std::ostream &out, const basic_sort &x)
Definition basic_sort.h:78
std::set< data::variable > find_all_variables(const data::data_expression_list &x)
Definition data.cpp:94
std::string pp(const data::list_container &x, bool arg0)
Definition data.cpp:63
std::set< data::sort_expression > find_sort_expressions(const data::data_expression &x)
Definition data.cpp:91
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:89
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)
Definition basic_sort.h:65
void swap(basic_sort &t1, basic_sort &t2) noexcept
\brief swap overload
Definition basic_sort.h:84
std::string pp(const data::container_type &x, bool arg0)
Definition data.cpp:49
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:93
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)
Definition data.cpp:67
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)
Definition data.cpp:77
data::data_expression translate_user_notation(const data::data_expression &x)
Definition data.cpp:88
std::string pp(const data::sort_expression_vector &x, bool arg0)
Definition data.cpp:25
std::string pp(const data::untyped_sort &x, bool arg0)
Definition data.cpp:78
std::string pp(const data::data_equation &x, bool arg0)
Definition data.cpp:50
std::string pp(const data::forall &x, bool arg0)
Definition data.cpp:56
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)
Definition data.cpp:28
std::string pp(const data::untyped_identifier &x, bool arg0)
Definition data.cpp:73
std::string pp(const data::function_symbol_list &x, bool arg0)
Definition data.cpp:32
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)
Definition data.cpp:62
std::ostream & operator<<(std::ostream &out, const alias &x)
Definition alias.h:91
std::set< data::variable > find_all_variables(const data::function_symbol &x)
Definition data.cpp:95
std::string pp(const data::application &x, bool arg0)
Definition data.cpp:40
std::string pp(const data::function_sort &x, bool arg0)
Definition data.cpp:59
void make_alias(atermpp::aterm &t, const ARGUMENTS &... args)
Definition alias.h:63
std::string pp(const data::abstraction &x, bool arg0)
Definition data.cpp:38
std::string pp(const data::bag_comprehension_binder &x, bool arg0)
Definition data.cpp:44
std::string pp(const data::set_comprehension_binder &x, bool arg0)
Definition data.cpp:66
std::string pp(const data::assignment &x, bool arg0)
Definition data.cpp:41
std::string pp(const data::structured_sort &x, bool arg0)
Definition data.cpp:69
std::string pp(const data::basic_sort &x, bool arg0)
Definition data.cpp:46
std::string pp(const data::exists_binder &x, bool arg0)
Definition data.cpp:54
std::string pp(const data::bag_comprehension &x, bool arg0)
Definition data.cpp:43
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)
Definition data.cpp:80
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)
Definition data.cpp:81
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:90
std::set< data::function_symbol > find_function_symbols(const data::data_equation &x)
Definition data.cpp:100
std::string pp(const data::bag_container &x, bool arg0)
Definition data.cpp:45
std::string pp(const data::alias &x, bool arg0)
Definition data.cpp:39
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:98
void swap(sort_expression &t1, sort_expression &t2) noexcept
\brief swap overload
std::set< data::variable > find_all_variables(const data::variable_list &x)
Definition data.cpp:97
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
Definition alias.h:97
bool is_assignment(const atermpp::aterm &x)
Definition assignment.h:152
std::string pp(const data::structured_sort_constructor &x, bool arg0)
Definition data.cpp:70
std::set< data::sort_expression > find_sort_expressions(const data::sort_expression &x)
Definition data.cpp:92
std::string pp(const data::data_specification &x, bool arg0)
Definition data.cpp:52
std::string pp(const data::data_equation_list &x, bool arg0)
Definition data.cpp:36
std::string pp(const data::fset_container &x, bool arg0)
Definition data.cpp:58
std::string pp(const data::sort_expression &x, bool arg0)
Definition data.cpp:68
std::string pp(const data::untyped_set_or_bag_comprehension &x, bool arg0)
Definition data.cpp:76
std::pair< basic_sort_vector, alias_vector > parse_sort_specification(const std::string &text)
Definition data.cpp:251
data::sort_expression normalize_sorts(const data::sort_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
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)
Definition data.cpp:30
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)
Definition data.cpp:99
std::string pp(const data::data_expression &x, bool arg0)
Definition data.cpp:51
std::string pp(const data::lambda &x, bool arg0)
Definition data.cpp:61
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)
Definition data.cpp:55
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)
Definition data.cpp:34
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)
Definition data.cpp:48
data::variable_list normalize_sorts(const data::variable_list &x, const data::sort_specification &sortspec)
Definition data.cpp:87
data::data_expression normalize_sorts(const data::data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:85
std::string pp(const data::untyped_sort_variable &x, bool arg0)
Definition data.cpp:79
std::string pp(const data::untyped_data_parameter &x, bool arg0)
Definition data.cpp:72
std::string pp(const data::binder_type &x, bool arg0)
Definition data.cpp:47
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)
Definition assignment.h:248
bool is_alias(const atermpp::aterm &x)
Definition alias.h:78
std::set< data::variable > find_all_variables(const data::variable &x)
Definition data.cpp:96
std::set< core::identifier_string > find_identifiers(const data::variable_list &x)
Definition data.cpp:101
std::ostream & operator<<(std::ostream &out, const sort_expression &x)
bool search_variable(const data::data_expression &x, const data::variable &v)
Definition data.cpp:102
std::string pp(const data::sort_expression_list &x, bool arg0)
Definition data.cpp:24
std::string pp(const data::forall_binder &x, bool arg0)
Definition data.cpp:57
std::string pp(const data::untyped_possible_sorts &x, bool arg0)
Definition data.cpp:75
std::string pp(const data::function_symbol &x, bool arg0)
Definition data.cpp:60
std::set< data::variable > substitution_variables(const mutable_map_substitution<> &sigma)
Definition data.cpp:184
std::string pp(const data::machine_number &x, bool arg0)
Definition data.cpp:64
std::string pp(const data::assignment_expression &x, bool arg0)
Definition data.cpp:42
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)
Definition data.cpp:65
std::string pp(const data::data_expression_list &x, bool arg0)
Definition data.cpp:26
expression builder that visits all sub expressions
Definition builder.h:32
void leave(const T &)
Definition builder.h:40
void enter(const T &)
Definition builder.h:35
static const atermpp::aterm SortExpr
static const atermpp::aterm SortId
static const atermpp::aterm SortRef
void apply(T &result, const argument_type &x)
Definition builder.h:173
update_apply_builder(const Function &f)
Definition builder.h:179
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:511
void apply(T &result, const data::machine_number &x)
Definition builder.h:445
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:471
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:578
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:519
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:454
void apply(T &result, const data::data_equation &x)
Definition builder.h:527
void apply(T &result, const data::function_symbol &x)
Definition builder.h:416
void apply(T &result, const data::assignment &x)
Definition builder.h:463
void apply(T &result, const data::abstraction &x)
Definition builder.h:593
void apply(T &result, const data::forall &x)
Definition builder.h:479
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:535
void apply(T &result, const data::exists &x)
Definition builder.h:487
void apply(T &result, const data::where_clause &x)
Definition builder.h:437
void apply(T &result, const data::application &x)
Definition builder.h:425
void apply(T &result, const data::variable &x)
Definition builder.h:407
void apply(T &result, const data::data_expression &x)
Definition builder.h:543
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:503
void apply(T &result, const data::lambda &x)
Definition builder.h:495
void apply(T &result, const data::assignment &x)
Definition builder.h:108
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:207
void apply(T &result, const data::structured_sort_constructor_argument &x)
Definition builder.h:231
void apply(T &result, const data::container_sort &x)
Definition builder.h:133
void apply(T &result, const data::alias &x)
Definition builder.h:247
void apply(T &result, const data::exists &x)
Definition builder.h:191
void apply(T &result, const data::machine_number &x)
Definition builder.h:90
void apply(T &result, const data::function_symbol &x)
Definition builder.h:62
void apply(T &result, const data::untyped_possible_sorts &x)
Definition builder.h:166
void apply(T &result, const data::forall &x)
Definition builder.h:183
void apply(T &result, const data::basic_sort &x)
Definition builder.h:124
void apply(T &result, const data::data_equation &x)
Definition builder.h:255
void apply(T &result, const data::untyped_sort &x)
Definition builder.h:157
void apply(T &result, const data::abstraction &x)
Definition builder.h:356
void apply(T &result, const data::application &x)
Definition builder.h:70
void apply(T &result, const data::variable &x)
Definition builder.h:54
void apply(T &result, const data::structured_sort &x)
Definition builder.h:141
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:116
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:263
void apply(T &result, const data::function_sort &x)
Definition builder.h:149
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:99
void apply(T &result, const data::structured_sort_constructor &x)
Definition builder.h:239
void apply(T &result, const data::lambda &x)
Definition builder.h:199
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:223
void apply(T &result, const data::where_clause &x)
Definition builder.h:82
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:306
void apply(T &result, const data::data_expression &x)
Definition builder.h:271
void apply(T &result, const data::sort_expression &x)
Definition builder.h:321
void apply(T &result, const data::untyped_sort_variable &x)
Definition builder.h:174
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:215
void apply(T &result, const data::abstraction &x)
Definition builder.h:829
void apply(T &result, const data::application &x)
Definition builder.h:661
void apply(T &result, const data::untyped_data_parameter &x)
Definition builder.h:771
void apply(T &result, const data::untyped_identifier &x)
Definition builder.h:690
void apply(T &result, const data::data_expression &x)
Definition builder.h:779
void apply(T &result, const data::assignment_expression &x)
Definition builder.h:814
void apply(T &result, const data::where_clause &x)
Definition builder.h:673
void apply(T &result, const data::forall &x)
Definition builder.h:715
void apply(T &result, const data::function_symbol &x)
Definition builder.h:652
void apply(T &result, const data::exists &x)
Definition builder.h:723
void apply(T &result, const data::lambda &x)
Definition builder.h:731
void apply(T &result, const data::variable &x)
Definition builder.h:643
void apply(T &result, const data::assignment &x)
Definition builder.h:699
void apply(T &result, const data::untyped_identifier_assignment &x)
Definition builder.h:707
void apply(T &result, const data::untyped_set_or_bag_comprehension &x)
Definition builder.h:755
void apply(T &result, const data::set_comprehension &x)
Definition builder.h:739
void apply(T &result, const data::bag_comprehension &x)
Definition builder.h:747
void apply(T &result, const data::machine_number &x)
Definition builder.h:681
void apply(T &result, const data::data_equation &x)
Definition builder.h:763
data_expression_actions(const core::parser &parser_)
Definition parse_impl.h:138
data::data_expression parse_DataExpr(const core::parse_node &node) const
Definition parse_impl.h:208
data_specification_actions(const core::parser &parser_)
Definition parse_impl.h:297
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
Definition parse_impl.h:458
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
Definition parse_impl.h:32
\brief Builder class
Definition builder.h:864
std::size_t operator()(const mcrl2::data::sort_expression &x) const