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//
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
20
21namespace mcrl2
22{
23
24namespace core
25{
26
27namespace detail
28{
29
30// checks
31// 1) if term t satisfies the predicate f
32template <typename Term, typename CheckFunction>
33bool check_term_argument(const Term& t, CheckFunction f)
34{
35 return f(t);
36}
37
38// checks
39// 1) if term t is a list,
40// 2) if the list has the proper minimum size
41// 3) if all elements of the list satisfy the predicate f
42template <typename Term, typename CheckFunction>
43bool check_list_argument(const Term& t, CheckFunction f, unsigned int minimum_size)
44{
45 const atermpp::aterm& term(t);
46 if (!t.type_is_list())
47 {
48 return false;
49 }
50 const atermpp::aterm_list& l = atermpp::down_cast<atermpp::aterm_list>(term);
51 if (l.size() < minimum_size)
52 {
53 return false;
54 }
55 for (const auto& x: l)
56 {
57 if (!f(x))
58 {
59 return false;
60 }
61 }
62 return true;
63}
64
65template <typename Term>
66bool check_rule_String(const Term& t)
67{
68 const atermpp::aterm& term(t);
69 if (!term.type_is_appl())
70 {
71 return false;
72 }
73 if (term.size() > 0)
74 {
75 return false;
76 }
77 if (term == atermpp::empty_string())
78 {
79 return false;
80 }
81 return true;
82}
83
84template <typename Term>
85bool check_rule_StringOrEmpty(const Term& t)
86{
87 const atermpp::aterm& term(t);
88 if (!term.type_is_appl())
89 {
90 return false;
91 }
92 return term.size() <= 0;
93}
94
95template <typename Term>
96bool check_rule_Number(const Term& t)
97{
98 const atermpp::aterm& term(t);
99 return term.type_is_int();
100}
101
102template <typename Term> bool check_rule_DataExpr(const Term& t);
103
104// DataAppl(DataExpr, DataExpr+)
105template <typename Term>
106bool check_term_DataAppl(const Term& t)
107{
109#ifndef MCRL2_NO_SOUNDNESS_CHECKS
110 // check the type of the term
111 const atermpp::aterm& term(t);
112 if (term.type_is_int())
113 {
114 return true;
115 }
116 if (!term.type_is_appl())
117 {
118 return false;
119 }
120 if (!gsIsDataAppl(term))
121 {
122 return false;
123 }
124#ifndef LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
125 for (const atermpp::aterm& child : term)
126 {
127 if (!check_term_argument(child, check_rule_DataExpr<atermpp::aterm>))
128 {
129 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
130 return false;
131 }
132 }
133#endif // LPS_NO_RECURSIVE_SOUNDNESS_CHECKS
134
135#endif // MCRL2_NO_SOUNDNESS_CHECKS
136 return true;
137}
138
139//--- start generated code ---//
140template <typename Term> bool check_rule_SortExpr(const Term& t);
141template <typename Term> bool check_rule_SortId(const Term& t);
142template <typename Term> bool check_rule_SortConsType(const Term& t);
143template <typename Term> bool check_rule_StructCons(const Term& t);
144template <typename Term> bool check_rule_StructProj(const Term& t);
145template <typename Term> bool check_rule_DataExpr(const Term& t);
146template <typename Term> bool check_rule_DataVarId(const Term& t);
147template <typename Term> bool check_rule_OpId(const Term& t);
148template <typename Term> bool check_rule_UntypedDataParameter(const Term& t);
149template <typename Term> bool check_rule_BindingOperator(const Term& t);
150template <typename Term> bool check_rule_WhrDecl(const Term& t);
151template <typename Term> bool check_rule_DataVarIdInit(const Term& t);
152template <typename Term> bool check_rule_UntypedIdentifierAssignment(const Term& t);
153template <typename Term> bool check_rule_DataSpec(const Term& t);
154template <typename Term> bool check_rule_SortSpec(const Term& t);
155template <typename Term> bool check_rule_ConsSpec(const Term& t);
156template <typename Term> bool check_rule_MapSpec(const Term& t);
157template <typename Term> bool check_rule_DataEqnSpec(const Term& t);
158template <typename Term> bool check_rule_SortDecl(const Term& t);
159template <typename Term> bool check_rule_DataEqn(const Term& t);
160template <typename Term> bool check_rule_MultAct(const Term& t);
161template <typename Term> bool check_rule_TimedMultAct(const Term& t);
162template <typename Term> bool check_rule_UntypedMultiAction(const Term& t);
163template <typename Term> bool check_rule_Action(const Term& t);
164template <typename Term> bool check_rule_ActId(const Term& t);
165template <typename Term> bool check_rule_ProcExpr(const Term& t);
166template <typename Term> bool check_rule_ProcVarId(const Term& t);
167template <typename Term> bool check_rule_MultActName(const Term& t);
168template <typename Term> bool check_rule_RenameExpr(const Term& t);
169template <typename Term> bool check_rule_CommExpr(const Term& t);
170template <typename Term> bool check_rule_ProcSpec(const Term& t);
171template <typename Term> bool check_rule_ActSpec(const Term& t);
172template <typename Term> bool check_rule_GlobVarSpec(const Term& t);
173template <typename Term> bool check_rule_ProcEqnSpec(const Term& t);
174template <typename Term> bool check_rule_ProcEqn(const Term& t);
175template <typename Term> bool check_rule_MultActOrDelta(const Term& t);
176template <typename Term> bool check_rule_ProcInit(const Term& t);
177template <typename Term> bool check_rule_Distribution(const Term& t);
178template <typename Term> bool check_rule_LinProcSpec(const Term& t);
179template <typename Term> bool check_rule_LinearProcess(const Term& t);
180template <typename Term> bool check_rule_LinearProcessSummand(const Term& t);
181template <typename Term> bool check_rule_LinearProcessInit(const Term& t);
182template <typename Term> bool check_rule_StateFrm(const Term& t);
183template <typename Term> bool check_rule_RegFrm(const Term& t);
184template <typename Term> bool check_rule_ActFrm(const Term& t);
185template <typename Term> bool check_rule_ParamIdOrAction(const Term& t);
186template <typename Term> bool check_rule_ActionRenameRules(const Term& t);
187template <typename Term> bool check_rule_ActionRenameRule(const Term& t);
188template <typename Term> bool check_rule_ActionRenameRuleRHS(const Term& t);
189template <typename Term> bool check_rule_ActionRenameSpec(const Term& t);
190template <typename Term> bool check_rule_PBES(const Term& t);
191template <typename Term> bool check_rule_PBEqnSpec(const Term& t);
192template <typename Term> bool check_rule_PBInit(const Term& t);
193template <typename Term> bool check_rule_PBEqn(const Term& t);
194template <typename Term> bool check_rule_FixPoint(const Term& t);
195template <typename Term> bool check_rule_PropVarDecl(const Term& t);
196template <typename Term> bool check_rule_PBExpr(const Term& t);
197template <typename Term> bool check_rule_PropVarInst(const Term& t);
198template <typename Term> bool check_rule_PRES(const Term& t);
199template <typename Term> bool check_rule_PREqnSpec(const Term& t);
200template <typename Term> bool check_rule_PRInit(const Term& t);
201template <typename Term> bool check_rule_PREqn(const Term& t);
202template <typename Term> bool check_rule_PRExpr(const Term& t);
203template <typename Term> bool check_term_SortCons(const Term& t);
204template <typename Term> bool check_term_SortStruct(const Term& t);
205template <typename Term> bool check_term_SortArrow(const Term& t);
206template <typename Term> bool check_term_UntypedSortUnknown(const Term& t);
207template <typename Term> bool check_term_UntypedSortsPossible(const Term& t);
208template <typename Term> bool check_term_UntypedSortVariable(const Term& t);
209template <typename Term> bool check_term_SortId(const Term& t);
210template <typename Term> bool check_term_SortList(const Term& t);
211template <typename Term> bool check_term_SortSet(const Term& t);
212template <typename Term> bool check_term_SortBag(const Term& t);
213template <typename Term> bool check_term_SortFSet(const Term& t);
214template <typename Term> bool check_term_SortFBag(const Term& t);
215template <typename Term> bool check_term_StructCons(const Term& t);
216template <typename Term> bool check_term_StructProj(const Term& t);
217template <typename Term> bool check_term_Binder(const Term& t);
218template <typename Term> bool check_term_Whr(const Term& t);
219template <typename Term> bool check_term_UntypedIdentifier(const Term& t);
220template <typename Term> bool check_term_DataVarId(const Term& t);
221template <typename Term> bool check_term_OpId(const Term& t);
222template <typename Term> bool check_term_UntypedDataParameter(const Term& t);
223template <typename Term> bool check_term_Forall(const Term& t);
224template <typename Term> bool check_term_Exists(const Term& t);
225template <typename Term> bool check_term_SetComp(const Term& t);
226template <typename Term> bool check_term_BagComp(const Term& t);
227template <typename Term> bool check_term_Lambda(const Term& t);
228template <typename Term> bool check_term_UntypedSetBagComp(const Term& t);
229template <typename Term> bool check_term_DataVarIdInit(const Term& t);
230template <typename Term> bool check_term_UntypedIdentifierAssignment(const Term& t);
231template <typename Term> bool check_term_DataSpec(const Term& t);
232template <typename Term> bool check_term_SortSpec(const Term& t);
233template <typename Term> bool check_term_ConsSpec(const Term& t);
234template <typename Term> bool check_term_MapSpec(const Term& t);
235template <typename Term> bool check_term_DataEqnSpec(const Term& t);
236template <typename Term> bool check_term_SortRef(const Term& t);
237template <typename Term> bool check_term_DataEqn(const Term& t);
238template <typename Term> bool check_term_MultAct(const Term& t);
239template <typename Term> bool check_term_TimedMultAct(const Term& t);
240template <typename Term> bool check_term_UntypedMultiAction(const Term& t);
241template <typename Term> bool check_term_Action(const Term& t);
242template <typename Term> bool check_term_ActId(const Term& t);
243template <typename Term> bool check_term_Process(const Term& t);
244template <typename Term> bool check_term_ProcessAssignment(const Term& t);
245template <typename Term> bool check_term_Delta(const Term& t);
246template <typename Term> bool check_term_Tau(const Term& t);
247template <typename Term> bool check_term_Sum(const Term& t);
248template <typename Term> bool check_term_Block(const Term& t);
249template <typename Term> bool check_term_Hide(const Term& t);
250template <typename Term> bool check_term_Rename(const Term& t);
251template <typename Term> bool check_term_Comm(const Term& t);
252template <typename Term> bool check_term_Allow(const Term& t);
253template <typename Term> bool check_term_Sync(const Term& t);
254template <typename Term> bool check_term_AtTime(const Term& t);
255template <typename Term> bool check_term_Seq(const Term& t);
256template <typename Term> bool check_term_IfThen(const Term& t);
257template <typename Term> bool check_term_IfThenElse(const Term& t);
258template <typename Term> bool check_term_BInit(const Term& t);
259template <typename Term> bool check_term_Merge(const Term& t);
260template <typename Term> bool check_term_LMerge(const Term& t);
261template <typename Term> bool check_term_Choice(const Term& t);
262template <typename Term> bool check_term_StochasticOperator(const Term& t);
263template <typename Term> bool check_term_UntypedProcessAssignment(const Term& t);
264template <typename Term> bool check_term_ProcVarId(const Term& t);
265template <typename Term> bool check_term_MultActName(const Term& t);
266template <typename Term> bool check_term_RenameExpr(const Term& t);
267template <typename Term> bool check_term_CommExpr(const Term& t);
268template <typename Term> bool check_term_ProcSpec(const Term& t);
269template <typename Term> bool check_term_ActSpec(const Term& t);
270template <typename Term> bool check_term_GlobVarSpec(const Term& t);
271template <typename Term> bool check_term_ProcEqnSpec(const Term& t);
272template <typename Term> bool check_term_ProcEqn(const Term& t);
273template <typename Term> bool check_term_ProcessInit(const Term& t);
274template <typename Term> bool check_term_Distribution(const Term& t);
275template <typename Term> bool check_term_LinProcSpec(const Term& t);
276template <typename Term> bool check_term_LinearProcess(const Term& t);
277template <typename Term> bool check_term_LinearProcessSummand(const Term& t);
278template <typename Term> bool check_term_LinearProcessInit(const Term& t);
279template <typename Term> bool check_term_StateTrue(const Term& t);
280template <typename Term> bool check_term_StateFalse(const Term& t);
281template <typename Term> bool check_term_StateNot(const Term& t);
282template <typename Term> bool check_term_StateMinus(const Term& t);
283template <typename Term> bool check_term_StateAnd(const Term& t);
284template <typename Term> bool check_term_StateOr(const Term& t);
285template <typename Term> bool check_term_StateImp(const Term& t);
286template <typename Term> bool check_term_StatePlus(const Term& t);
287template <typename Term> bool check_term_StateConstantMultiply(const Term& t);
288template <typename Term> bool check_term_StateConstantMultiplyAlt(const Term& t);
289template <typename Term> bool check_term_StateForall(const Term& t);
290template <typename Term> bool check_term_StateExists(const Term& t);
291template <typename Term> bool check_term_StateInfimum(const Term& t);
292template <typename Term> bool check_term_StateSupremum(const Term& t);
293template <typename Term> bool check_term_StateSum(const Term& t);
294template <typename Term> bool check_term_StateMust(const Term& t);
295template <typename Term> bool check_term_StateMay(const Term& t);
296template <typename Term> bool check_term_StateYaled(const Term& t);
297template <typename Term> bool check_term_StateYaledTimed(const Term& t);
298template <typename Term> bool check_term_StateDelay(const Term& t);
299template <typename Term> bool check_term_StateDelayTimed(const Term& t);
300template <typename Term> bool check_term_StateVar(const Term& t);
301template <typename Term> bool check_term_StateNu(const Term& t);
302template <typename Term> bool check_term_StateMu(const Term& t);
303template <typename Term> bool check_term_RegNil(const Term& t);
304template <typename Term> bool check_term_RegSeq(const Term& t);
305template <typename Term> bool check_term_RegAlt(const Term& t);
306template <typename Term> bool check_term_RegTrans(const Term& t);
307template <typename Term> bool check_term_RegTransOrNil(const Term& t);
308template <typename Term> bool check_term_UntypedRegFrm(const Term& t);
309template <typename Term> bool check_term_ActTrue(const Term& t);
310template <typename Term> bool check_term_ActFalse(const Term& t);
311template <typename Term> bool check_term_ActNot(const Term& t);
312template <typename Term> bool check_term_ActAnd(const Term& t);
313template <typename Term> bool check_term_ActOr(const Term& t);
314template <typename Term> bool check_term_ActImp(const Term& t);
315template <typename Term> bool check_term_ActForall(const Term& t);
316template <typename Term> bool check_term_ActExists(const Term& t);
317template <typename Term> bool check_term_ActAt(const Term& t);
318template <typename Term> bool check_term_ActMultAct(const Term& t);
319template <typename Term> bool check_term_ActionRenameRules(const Term& t);
320template <typename Term> bool check_term_ActionRenameRule(const Term& t);
321template <typename Term> bool check_term_ActionRenameSpec(const Term& t);
322template <typename Term> bool check_term_PBES(const Term& t);
323template <typename Term> bool check_term_PBEqnSpec(const Term& t);
324template <typename Term> bool check_term_PBInit(const Term& t);
325template <typename Term> bool check_term_PBEqn(const Term& t);
326template <typename Term> bool check_term_Mu(const Term& t);
327template <typename Term> bool check_term_Nu(const Term& t);
328template <typename Term> bool check_term_PropVarDecl(const Term& t);
329template <typename Term> bool check_term_PBESTrue(const Term& t);
330template <typename Term> bool check_term_PBESFalse(const Term& t);
331template <typename Term> bool check_term_PBESNot(const Term& t);
332template <typename Term> bool check_term_PBESAnd(const Term& t);
333template <typename Term> bool check_term_PBESOr(const Term& t);
334template <typename Term> bool check_term_PBESImp(const Term& t);
335template <typename Term> bool check_term_PBESForall(const Term& t);
336template <typename Term> bool check_term_PBESExists(const Term& t);
337template <typename Term> bool check_term_PropVarInst(const Term& t);
338template <typename Term> bool check_term_PRES(const Term& t);
339template <typename Term> bool check_term_PREqnSpec(const Term& t);
340template <typename Term> bool check_term_PRInit(const Term& t);
341template <typename Term> bool check_term_PREqn(const Term& t);
342template <typename Term> bool check_term_PRESTrue(const Term& t);
343template <typename Term> bool check_term_PRESFalse(const Term& t);
344template <typename Term> bool check_term_PRESMinus(const Term& t);
345template <typename Term> bool check_term_PRESAnd(const Term& t);
346template <typename Term> bool check_term_PRESOr(const Term& t);
347template <typename Term> bool check_term_PRESImp(const Term& t);
348template <typename Term> bool check_term_PRESPlus(const Term& t);
349template <typename Term> bool check_term_PRESConstantMultiply(const Term& t);
350template <typename Term> bool check_term_PRESConstantMultiplyAlt(const Term& t);
351template <typename Term> bool check_term_PRESInfimum(const Term& t);
352template <typename Term> bool check_term_PRESSupremum(const Term& t);
353template <typename Term> bool check_term_PRESSum(const Term& t);
354template <typename Term> bool check_term_PRESEqInf(const Term& t);
355template <typename Term> bool check_term_PRESEqNInf(const Term& t);
356template <typename Term> bool check_term_PRESCondSm(const Term& t);
357template <typename Term> bool check_term_PRESCondEq(const Term& t);
358
359template <typename Term>
360bool check_rule_SortExpr(const Term& t)
361{
363#ifndef MCRL2_NO_SOUNDNESS_CHECKS
364 return check_rule_SortId(t)
371#else
372 return true;
373#endif // MCRL2_NO_SOUNDNESS_CHECKS
374}
375
376template <typename Term>
377bool check_rule_SortId(const Term& t)
378{
380#ifndef MCRL2_NO_SOUNDNESS_CHECKS
381 return check_term_SortId(t);
382#else
383 return true;
384#endif // MCRL2_NO_SOUNDNESS_CHECKS
385}
386
387template <typename Term>
388bool check_rule_SortConsType(const Term& t)
389{
391#ifndef MCRL2_NO_SOUNDNESS_CHECKS
392 return check_term_SortList(t)
397#else
398 return true;
399#endif // MCRL2_NO_SOUNDNESS_CHECKS
400}
401
402template <typename Term>
403bool check_rule_StructCons(const Term& t)
404{
406#ifndef MCRL2_NO_SOUNDNESS_CHECKS
407 return check_term_StructCons(t);
408#else
409 return true;
410#endif // MCRL2_NO_SOUNDNESS_CHECKS
411}
412
413template <typename Term>
414bool check_rule_StructProj(const Term& t)
415{
417#ifndef MCRL2_NO_SOUNDNESS_CHECKS
418 return check_term_StructProj(t);
419#else
420 return true;
421#endif // MCRL2_NO_SOUNDNESS_CHECKS
422}
423
424template <typename Term>
425bool check_rule_DataExpr(const Term& t)
426{
428#ifndef MCRL2_NO_SOUNDNESS_CHECKS
429 return check_rule_DataVarId(t)
430 || check_rule_OpId(t)
433 || check_term_Whr(t)
435#else
436 return true;
437#endif // MCRL2_NO_SOUNDNESS_CHECKS
438}
439
440template <typename Term>
441bool check_rule_DataVarId(const Term& t)
442{
444#ifndef MCRL2_NO_SOUNDNESS_CHECKS
445 return check_term_DataVarId(t);
446#else
447 return true;
448#endif // MCRL2_NO_SOUNDNESS_CHECKS
449}
450
451template <typename Term>
452bool check_rule_OpId(const Term& t)
453{
455#ifndef MCRL2_NO_SOUNDNESS_CHECKS
456 return check_term_OpId(t);
457#else
458 return true;
459#endif // MCRL2_NO_SOUNDNESS_CHECKS
460}
461
462template <typename Term>
464{
466#ifndef MCRL2_NO_SOUNDNESS_CHECKS
468#else
469 return true;
470#endif // MCRL2_NO_SOUNDNESS_CHECKS
471}
472
473template <typename Term>
474bool check_rule_BindingOperator(const Term& t)
475{
477#ifndef MCRL2_NO_SOUNDNESS_CHECKS
478 return check_term_Forall(t)
484#else
485 return true;
486#endif // MCRL2_NO_SOUNDNESS_CHECKS
487}
488
489template <typename Term>
490bool check_rule_WhrDecl(const Term& t)
491{
493#ifndef MCRL2_NO_SOUNDNESS_CHECKS
496#else
497 return true;
498#endif // MCRL2_NO_SOUNDNESS_CHECKS
499}
500
501template <typename Term>
502bool check_rule_DataVarIdInit(const Term& t)
503{
505#ifndef MCRL2_NO_SOUNDNESS_CHECKS
506 return check_term_DataVarIdInit(t);
507#else
508 return true;
509#endif // MCRL2_NO_SOUNDNESS_CHECKS
510}
511
512template <typename Term>
514{
516#ifndef MCRL2_NO_SOUNDNESS_CHECKS
518#else
519 return true;
520#endif // MCRL2_NO_SOUNDNESS_CHECKS
521}
522
523template <typename Term>
524bool check_rule_DataSpec(const Term& t)
525{
527#ifndef MCRL2_NO_SOUNDNESS_CHECKS
528 return check_term_DataSpec(t);
529#else
530 return true;
531#endif // MCRL2_NO_SOUNDNESS_CHECKS
532}
533
534template <typename Term>
535bool check_rule_SortSpec(const Term& t)
536{
538#ifndef MCRL2_NO_SOUNDNESS_CHECKS
539 return check_term_SortSpec(t);
540#else
541 return true;
542#endif // MCRL2_NO_SOUNDNESS_CHECKS
543}
544
545template <typename Term>
546bool check_rule_ConsSpec(const Term& t)
547{
549#ifndef MCRL2_NO_SOUNDNESS_CHECKS
550 return check_term_ConsSpec(t);
551#else
552 return true;
553#endif // MCRL2_NO_SOUNDNESS_CHECKS
554}
555
556template <typename Term>
557bool check_rule_MapSpec(const Term& t)
558{
560#ifndef MCRL2_NO_SOUNDNESS_CHECKS
561 return check_term_MapSpec(t);
562#else
563 return true;
564#endif // MCRL2_NO_SOUNDNESS_CHECKS
565}
566
567template <typename Term>
568bool check_rule_DataEqnSpec(const Term& t)
569{
571#ifndef MCRL2_NO_SOUNDNESS_CHECKS
572 return check_term_DataEqnSpec(t);
573#else
574 return true;
575#endif // MCRL2_NO_SOUNDNESS_CHECKS
576}
577
578template <typename Term>
579bool check_rule_SortDecl(const Term& t)
580{
582#ifndef MCRL2_NO_SOUNDNESS_CHECKS
583 return check_rule_SortId(t)
584 || check_term_SortRef(t);
585#else
586 return true;
587#endif // MCRL2_NO_SOUNDNESS_CHECKS
588}
589
590template <typename Term>
591bool check_rule_DataEqn(const Term& t)
592{
594#ifndef MCRL2_NO_SOUNDNESS_CHECKS
595 return check_term_DataEqn(t);
596#else
597 return true;
598#endif // MCRL2_NO_SOUNDNESS_CHECKS
599}
600
601template <typename Term>
602bool check_rule_MultAct(const Term& t)
603{
605#ifndef MCRL2_NO_SOUNDNESS_CHECKS
606 return check_term_MultAct(t);
607#else
608 return true;
609#endif // MCRL2_NO_SOUNDNESS_CHECKS
610}
611
612template <typename Term>
613bool check_rule_TimedMultAct(const Term& t)
614{
616#ifndef MCRL2_NO_SOUNDNESS_CHECKS
617 return check_term_TimedMultAct(t);
618#else
619 return true;
620#endif // MCRL2_NO_SOUNDNESS_CHECKS
621}
622
623template <typename Term>
625{
627#ifndef MCRL2_NO_SOUNDNESS_CHECKS
629#else
630 return true;
631#endif // MCRL2_NO_SOUNDNESS_CHECKS
632}
633
634template <typename Term>
635bool check_rule_Action(const Term& t)
636{
638#ifndef MCRL2_NO_SOUNDNESS_CHECKS
639 return check_term_Action(t);
640#else
641 return true;
642#endif // MCRL2_NO_SOUNDNESS_CHECKS
643}
644
645template <typename Term>
646bool check_rule_ActId(const Term& t)
647{
649#ifndef MCRL2_NO_SOUNDNESS_CHECKS
650 return check_term_ActId(t);
651#else
652 return true;
653#endif // MCRL2_NO_SOUNDNESS_CHECKS
654}
655
656template <typename Term>
657bool check_rule_ProcExpr(const Term& t)
658{
660#ifndef MCRL2_NO_SOUNDNESS_CHECKS
661 return check_rule_Action(t)
664 || check_term_Delta(t)
665 || check_term_Tau(t)
666 || check_term_Sum(t)
667 || check_term_Block(t)
668 || check_term_Hide(t)
670 || check_term_Comm(t)
671 || check_term_Allow(t)
672 || check_term_Sync(t)
674 || check_term_Seq(t)
677 || check_term_BInit(t)
678 || check_term_Merge(t)
684#else
685 return true;
686#endif // MCRL2_NO_SOUNDNESS_CHECKS
687}
688
689template <typename Term>
690bool check_rule_ProcVarId(const Term& t)
691{
693#ifndef MCRL2_NO_SOUNDNESS_CHECKS
694 return check_term_ProcVarId(t);
695#else
696 return true;
697#endif // MCRL2_NO_SOUNDNESS_CHECKS
698}
699
700template <typename Term>
701bool check_rule_MultActName(const Term& t)
702{
704#ifndef MCRL2_NO_SOUNDNESS_CHECKS
705 return check_term_MultActName(t);
706#else
707 return true;
708#endif // MCRL2_NO_SOUNDNESS_CHECKS
709}
710
711template <typename Term>
712bool check_rule_RenameExpr(const Term& t)
713{
715#ifndef MCRL2_NO_SOUNDNESS_CHECKS
716 return check_term_RenameExpr(t);
717#else
718 return true;
719#endif // MCRL2_NO_SOUNDNESS_CHECKS
720}
721
722template <typename Term>
723bool check_rule_CommExpr(const Term& t)
724{
726#ifndef MCRL2_NO_SOUNDNESS_CHECKS
727 return check_term_CommExpr(t);
728#else
729 return true;
730#endif // MCRL2_NO_SOUNDNESS_CHECKS
731}
732
733template <typename Term>
734bool check_rule_ProcSpec(const Term& t)
735{
737#ifndef MCRL2_NO_SOUNDNESS_CHECKS
738 return check_term_ProcSpec(t);
739#else
740 return true;
741#endif // MCRL2_NO_SOUNDNESS_CHECKS
742}
743
744template <typename Term>
745bool check_rule_ActSpec(const Term& t)
746{
748#ifndef MCRL2_NO_SOUNDNESS_CHECKS
749 return check_term_ActSpec(t);
750#else
751 return true;
752#endif // MCRL2_NO_SOUNDNESS_CHECKS
753}
754
755template <typename Term>
756bool check_rule_GlobVarSpec(const Term& t)
757{
759#ifndef MCRL2_NO_SOUNDNESS_CHECKS
760 return check_term_GlobVarSpec(t);
761#else
762 return true;
763#endif // MCRL2_NO_SOUNDNESS_CHECKS
764}
765
766template <typename Term>
767bool check_rule_ProcEqnSpec(const Term& t)
768{
770#ifndef MCRL2_NO_SOUNDNESS_CHECKS
771 return check_term_ProcEqnSpec(t);
772#else
773 return true;
774#endif // MCRL2_NO_SOUNDNESS_CHECKS
775}
776
777template <typename Term>
778bool check_rule_ProcEqn(const Term& t)
779{
781#ifndef MCRL2_NO_SOUNDNESS_CHECKS
782 return check_term_ProcEqn(t);
783#else
784 return true;
785#endif // MCRL2_NO_SOUNDNESS_CHECKS
786}
787
788template <typename Term>
789bool check_rule_MultActOrDelta(const Term& t)
790{
792#ifndef MCRL2_NO_SOUNDNESS_CHECKS
793 return check_rule_MultAct(t)
794 || check_term_Delta(t);
795#else
796 return true;
797#endif // MCRL2_NO_SOUNDNESS_CHECKS
798}
799
800template <typename Term>
801bool check_rule_ProcInit(const Term& t)
802{
804#ifndef MCRL2_NO_SOUNDNESS_CHECKS
805 return check_term_ProcessInit(t);
806#else
807 return true;
808#endif // MCRL2_NO_SOUNDNESS_CHECKS
809}
810
811template <typename Term>
812bool check_rule_Distribution(const Term& t)
813{
815#ifndef MCRL2_NO_SOUNDNESS_CHECKS
816 return check_term_Distribution(t);
817#else
818 return true;
819#endif // MCRL2_NO_SOUNDNESS_CHECKS
820}
821
822template <typename Term>
823bool check_rule_LinProcSpec(const Term& t)
824{
826#ifndef MCRL2_NO_SOUNDNESS_CHECKS
827 return check_term_LinProcSpec(t);
828#else
829 return true;
830#endif // MCRL2_NO_SOUNDNESS_CHECKS
831}
832
833template <typename Term>
834bool check_rule_LinearProcess(const Term& t)
835{
837#ifndef MCRL2_NO_SOUNDNESS_CHECKS
838 return check_term_LinearProcess(t);
839#else
840 return true;
841#endif // MCRL2_NO_SOUNDNESS_CHECKS
842}
843
844template <typename Term>
846{
848#ifndef MCRL2_NO_SOUNDNESS_CHECKS
850#else
851 return true;
852#endif // MCRL2_NO_SOUNDNESS_CHECKS
853}
854
855template <typename Term>
857{
859#ifndef MCRL2_NO_SOUNDNESS_CHECKS
861#else
862 return true;
863#endif // MCRL2_NO_SOUNDNESS_CHECKS
864}
865
866template <typename Term>
867bool check_rule_StateFrm(const Term& t)
868{
870#ifndef MCRL2_NO_SOUNDNESS_CHECKS
871 return check_rule_DataExpr(t)
897#else
898 return true;
899#endif // MCRL2_NO_SOUNDNESS_CHECKS
900}
901
902template <typename Term>
903bool check_rule_RegFrm(const Term& t)
904{
906#ifndef MCRL2_NO_SOUNDNESS_CHECKS
907 return check_rule_ActFrm(t)
914#else
915 return true;
916#endif // MCRL2_NO_SOUNDNESS_CHECKS
917}
918
919template <typename Term>
920bool check_rule_ActFrm(const Term& t)
921{
923#ifndef MCRL2_NO_SOUNDNESS_CHECKS
924 return check_rule_DataExpr(t)
929 || check_term_ActOr(t)
933 || check_term_ActAt(t)
937#else
938 return true;
939#endif // MCRL2_NO_SOUNDNESS_CHECKS
940}
941
942template <typename Term>
943bool check_rule_ParamIdOrAction(const Term& t)
944{
946#ifndef MCRL2_NO_SOUNDNESS_CHECKS
948 || check_rule_Action(t);
949#else
950 return true;
951#endif // MCRL2_NO_SOUNDNESS_CHECKS
952}
953
954template <typename Term>
956{
958#ifndef MCRL2_NO_SOUNDNESS_CHECKS
960#else
961 return true;
962#endif // MCRL2_NO_SOUNDNESS_CHECKS
963}
964
965template <typename Term>
967{
969#ifndef MCRL2_NO_SOUNDNESS_CHECKS
971#else
972 return true;
973#endif // MCRL2_NO_SOUNDNESS_CHECKS
974}
975
976template <typename Term>
978{
980#ifndef MCRL2_NO_SOUNDNESS_CHECKS
983 || check_term_Delta(t)
984 || check_term_Tau(t);
985#else
986 return true;
987#endif // MCRL2_NO_SOUNDNESS_CHECKS
988}
989
990template <typename Term>
992{
994#ifndef MCRL2_NO_SOUNDNESS_CHECKS
996#else
997 return true;
998#endif // MCRL2_NO_SOUNDNESS_CHECKS
999}
1000
1001template <typename Term>
1002bool check_rule_PBES(const Term& t)
1003{
1005#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1006 return check_term_PBES(t);
1007#else
1008 return true;
1009#endif // MCRL2_NO_SOUNDNESS_CHECKS
1010}
1011
1012template <typename Term>
1013bool check_rule_PBEqnSpec(const Term& t)
1014{
1016#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1017 return check_term_PBEqnSpec(t);
1018#else
1019 return true;
1020#endif // MCRL2_NO_SOUNDNESS_CHECKS
1021}
1022
1023template <typename Term>
1024bool check_rule_PBInit(const Term& t)
1025{
1027#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1028 return check_term_PBInit(t);
1029#else
1030 return true;
1031#endif // MCRL2_NO_SOUNDNESS_CHECKS
1032}
1033
1034template <typename Term>
1035bool check_rule_PBEqn(const Term& t)
1036{
1038#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1039 return check_term_PBEqn(t);
1040#else
1041 return true;
1042#endif // MCRL2_NO_SOUNDNESS_CHECKS
1043}
1044
1045template <typename Term>
1046bool check_rule_FixPoint(const Term& t)
1047{
1049#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1050 return check_term_Mu(t)
1051 || check_term_Nu(t);
1052#else
1053 return true;
1054#endif // MCRL2_NO_SOUNDNESS_CHECKS
1055}
1056
1057template <typename Term>
1058bool check_rule_PropVarDecl(const Term& t)
1059{
1061#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1062 return check_term_PropVarDecl(t);
1063#else
1064 return true;
1065#endif // MCRL2_NO_SOUNDNESS_CHECKS
1066}
1067
1068template <typename Term>
1069bool check_rule_PBExpr(const Term& t)
1070{
1072#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1073 return check_rule_DataExpr(t)
1076 || check_term_PBESNot(t)
1077 || check_term_PBESAnd(t)
1078 || check_term_PBESOr(t)
1079 || check_term_PBESImp(t)
1084#else
1085 return true;
1086#endif // MCRL2_NO_SOUNDNESS_CHECKS
1087}
1088
1089template <typename Term>
1090bool check_rule_PropVarInst(const Term& t)
1091{
1093#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1094 return check_term_PropVarInst(t);
1095#else
1096 return true;
1097#endif // MCRL2_NO_SOUNDNESS_CHECKS
1098}
1099
1100template <typename Term>
1101bool check_rule_PRES(const Term& t)
1102{
1104#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1105 return check_term_PRES(t);
1106#else
1107 return true;
1108#endif // MCRL2_NO_SOUNDNESS_CHECKS
1109}
1110
1111template <typename Term>
1112bool check_rule_PREqnSpec(const Term& t)
1113{
1115#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1116 return check_term_PREqnSpec(t);
1117#else
1118 return true;
1119#endif // MCRL2_NO_SOUNDNESS_CHECKS
1120}
1121
1122template <typename Term>
1123bool check_rule_PRInit(const Term& t)
1124{
1126#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1127 return check_term_PRInit(t);
1128#else
1129 return true;
1130#endif // MCRL2_NO_SOUNDNESS_CHECKS
1131}
1132
1133template <typename Term>
1134bool check_rule_PREqn(const Term& t)
1135{
1137#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1138 return check_term_PREqn(t);
1139#else
1140 return true;
1141#endif // MCRL2_NO_SOUNDNESS_CHECKS
1142}
1143
1144template <typename Term>
1145bool check_rule_PRExpr(const Term& t)
1146{
1148#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1149 return check_rule_DataExpr(t)
1153 || check_term_PRESAnd(t)
1154 || check_term_PRESOr(t)
1155 || check_term_PRESImp(t)
1161 || check_term_PRESSum(t)
1168#else
1169 return true;
1170#endif // MCRL2_NO_SOUNDNESS_CHECKS
1171}
1172
1173// SortCons(SortConsType, SortExpr)
1174template <typename Term>
1175bool check_term_SortCons(const Term& t)
1176{
1178#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1179 // check the type of the term
1180 const atermpp::aterm& term(t);
1181 if (!term.type_is_appl())
1182 {
1183 return false;
1184 }
1186 {
1187 return false;
1188 }
1189
1190 // check the children
1191 if (term.size() != 2)
1192 {
1193 return false;
1194 }
1195#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1196 if (!check_term_argument(term[0], check_rule_SortConsType<atermpp::aterm>))
1197 {
1198 mCRL2log(log::debug) << "check_rule_SortConsType" << std::endl;
1199 return false;
1200 }
1201 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1202 {
1203 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
1204 return false;
1205 }
1206#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1207
1208#endif // MCRL2_NO_SOUNDNESS_CHECKS
1209 return true;
1210}
1211
1212// SortStruct(StructCons+)
1213template <typename Term>
1214bool check_term_SortStruct(const Term& t)
1215{
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 }
1225 {
1226 return false;
1227 }
1228
1229 // check the children
1230 if (term.size() != 1)
1231 {
1232 return false;
1233 }
1234#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1235 if (!check_list_argument(term[0], check_rule_StructCons<atermpp::aterm>, 1))
1236 {
1237 mCRL2log(log::debug) << "check_rule_StructCons" << std::endl;
1238 return false;
1239 }
1240#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1241
1242#endif // MCRL2_NO_SOUNDNESS_CHECKS
1243 return true;
1244}
1245
1246// SortArrow(SortExpr+, SortExpr)
1247template <typename Term>
1248bool check_term_SortArrow(const Term& t)
1249{
1251#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1252 // check the type of the term
1253 const atermpp::aterm& term(t);
1254 if (!term.type_is_appl())
1255 {
1256 return false;
1257 }
1259 {
1260 return false;
1261 }
1262
1263 // check the children
1264 if (term.size() != 2)
1265 {
1266 return false;
1267 }
1268#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1269 if (!check_list_argument(term[0], check_rule_SortExpr<atermpp::aterm>, 1))
1270 {
1271 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
1272 return false;
1273 }
1274 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1275 {
1276 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
1277 return false;
1278 }
1279#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1280
1281#endif // MCRL2_NO_SOUNDNESS_CHECKS
1282 return true;
1283}
1284
1285// UntypedSortUnknown()
1286template <typename Term>
1288{
1290#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1291 // check the type of the term
1292 const atermpp::aterm& term(t);
1293 if (!term.type_is_appl())
1294 {
1295 return false;
1296 }
1298 {
1299 return false;
1300 }
1301
1302 // check the children
1303 if (term.size() != 0)
1304 {
1305 return false;
1306 }
1307
1308#endif // MCRL2_NO_SOUNDNESS_CHECKS
1309 return true;
1310}
1311
1312// UntypedSortsPossible(SortExpr+)
1313template <typename Term>
1315{
1317#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1318 // check the type of the term
1319 const atermpp::aterm& term(t);
1320 if (!term.type_is_appl())
1321 {
1322 return false;
1323 }
1325 {
1326 return false;
1327 }
1328
1329 // check the children
1330 if (term.size() != 1)
1331 {
1332 return false;
1333 }
1334#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1335 if (!check_list_argument(term[0], check_rule_SortExpr<atermpp::aterm>, 1))
1336 {
1337 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
1338 return false;
1339 }
1340#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1341
1342#endif // MCRL2_NO_SOUNDNESS_CHECKS
1343 return true;
1344}
1345
1346// UntypedSortVariable(Number)
1347template <typename Term>
1349{
1351#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1352 // check the type of the term
1353 const atermpp::aterm& term(t);
1354 if (!term.type_is_appl())
1355 {
1356 return false;
1357 }
1359 {
1360 return false;
1361 }
1362
1363 // check the children
1364 if (term.size() != 1)
1365 {
1366 return false;
1367 }
1368#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1369 if (!check_term_argument(term[0], check_rule_Number<atermpp::aterm>))
1370 {
1371 mCRL2log(log::debug) << "check_rule_Number" << std::endl;
1372 return false;
1373 }
1374#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1375
1376#endif // MCRL2_NO_SOUNDNESS_CHECKS
1377 return true;
1378}
1379
1380// SortId(String)
1381template <typename Term>
1382bool check_term_SortId(const Term& t)
1383{
1385#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1386 // check the type of the term
1387 const atermpp::aterm& term(t);
1388 if (!term.type_is_appl())
1389 {
1390 return false;
1391 }
1393 {
1394 return false;
1395 }
1396
1397 // check the children
1398 if (term.size() != 1)
1399 {
1400 return false;
1401 }
1402#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1403 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1404 {
1405 mCRL2log(log::debug) << "check_rule_String" << std::endl;
1406 return false;
1407 }
1408#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1409
1410#endif // MCRL2_NO_SOUNDNESS_CHECKS
1411 return true;
1412}
1413
1414// SortList()
1415template <typename Term>
1416bool check_term_SortList(const Term& t)
1417{
1419#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1420 // check the type of the term
1421 const atermpp::aterm& term(t);
1422 if (!term.type_is_appl())
1423 {
1424 return false;
1425 }
1427 {
1428 return false;
1429 }
1430
1431 // check the children
1432 if (term.size() != 0)
1433 {
1434 return false;
1435 }
1436
1437#endif // MCRL2_NO_SOUNDNESS_CHECKS
1438 return true;
1439}
1440
1441// SortSet()
1442template <typename Term>
1443bool check_term_SortSet(const Term& t)
1444{
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 }
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// SortBag()
1469template <typename Term>
1470bool check_term_SortBag(const Term& t)
1471{
1473#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1474 // check the type of the term
1475 const atermpp::aterm& term(t);
1476 if (!term.type_is_appl())
1477 {
1478 return false;
1479 }
1481 {
1482 return false;
1483 }
1484
1485 // check the children
1486 if (term.size() != 0)
1487 {
1488 return false;
1489 }
1490
1491#endif // MCRL2_NO_SOUNDNESS_CHECKS
1492 return true;
1493}
1494
1495// SortFSet()
1496template <typename Term>
1497bool check_term_SortFSet(const Term& t)
1498{
1500#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1501 // check the type of the term
1502 const atermpp::aterm& term(t);
1503 if (!term.type_is_appl())
1504 {
1505 return false;
1506 }
1508 {
1509 return false;
1510 }
1511
1512 // check the children
1513 if (term.size() != 0)
1514 {
1515 return false;
1516 }
1517
1518#endif // MCRL2_NO_SOUNDNESS_CHECKS
1519 return true;
1520}
1521
1522// SortFBag()
1523template <typename Term>
1524bool check_term_SortFBag(const Term& t)
1525{
1527#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1528 // check the type of the term
1529 const atermpp::aterm& term(t);
1530 if (!term.type_is_appl())
1531 {
1532 return false;
1533 }
1535 {
1536 return false;
1537 }
1538
1539 // check the children
1540 if (term.size() != 0)
1541 {
1542 return false;
1543 }
1544
1545#endif // MCRL2_NO_SOUNDNESS_CHECKS
1546 return true;
1547}
1548
1549// StructCons(String, StructProj*, StringOrEmpty)
1550template <typename Term>
1551bool check_term_StructCons(const Term& t)
1552{
1554#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1555 // check the type of the term
1556 const atermpp::aterm& term(t);
1557 if (!term.type_is_appl())
1558 {
1559 return false;
1560 }
1562 {
1563 return false;
1564 }
1565
1566 // check the children
1567 if (term.size() != 3)
1568 {
1569 return false;
1570 }
1571#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1572 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1573 {
1574 mCRL2log(log::debug) << "check_rule_String" << std::endl;
1575 return false;
1576 }
1577 if (!check_list_argument(term[1], check_rule_StructProj<atermpp::aterm>, 0))
1578 {
1579 mCRL2log(log::debug) << "check_rule_StructProj" << std::endl;
1580 return false;
1581 }
1582 if (!check_term_argument(term[2], check_rule_StringOrEmpty<atermpp::aterm>))
1583 {
1584 mCRL2log(log::debug) << "check_rule_StringOrEmpty" << std::endl;
1585 return false;
1586 }
1587#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1588
1589#endif // MCRL2_NO_SOUNDNESS_CHECKS
1590 return true;
1591}
1592
1593// StructProj(StringOrEmpty, SortExpr)
1594template <typename Term>
1595bool check_term_StructProj(const Term& t)
1596{
1598#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1599 // check the type of the term
1600 const atermpp::aterm& term(t);
1601 if (!term.type_is_appl())
1602 {
1603 return false;
1604 }
1606 {
1607 return false;
1608 }
1609
1610 // check the children
1611 if (term.size() != 2)
1612 {
1613 return false;
1614 }
1615#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1616 if (!check_term_argument(term[0], check_rule_StringOrEmpty<atermpp::aterm>))
1617 {
1618 mCRL2log(log::debug) << "check_rule_StringOrEmpty" << std::endl;
1619 return false;
1620 }
1621 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1622 {
1623 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
1624 return false;
1625 }
1626#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1627
1628#endif // MCRL2_NO_SOUNDNESS_CHECKS
1629 return true;
1630}
1631
1632// Binder(BindingOperator, DataVarId+, DataExpr)
1633template <typename Term>
1634bool check_term_Binder(const Term& t)
1635{
1637#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1638 // check the type of the term
1639 const atermpp::aterm& term(t);
1640 if (!term.type_is_appl())
1641 {
1642 return false;
1643 }
1645 {
1646 return false;
1647 }
1648
1649 // check the children
1650 if (term.size() != 3)
1651 {
1652 return false;
1653 }
1654#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1655 if (!check_term_argument(term[0], check_rule_BindingOperator<atermpp::aterm>))
1656 {
1657 mCRL2log(log::debug) << "check_rule_BindingOperator" << std::endl;
1658 return false;
1659 }
1660 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 1))
1661 {
1662 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
1663 return false;
1664 }
1665 if (!check_term_argument(term[2], check_rule_DataExpr<atermpp::aterm>))
1666 {
1667 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
1668 return false;
1669 }
1670#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1671
1672#endif // MCRL2_NO_SOUNDNESS_CHECKS
1673 return true;
1674}
1675
1676// Whr(DataExpr, WhrDecl+)
1677template <typename Term>
1678bool check_term_Whr(const Term& t)
1679{
1681#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1682 // check the type of the term
1683 const atermpp::aterm& term(t);
1684 if (!term.type_is_appl())
1685 {
1686 return false;
1687 }
1689 {
1690 return false;
1691 }
1692
1693 // check the children
1694 if (term.size() != 2)
1695 {
1696 return false;
1697 }
1698#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1699 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
1700 {
1701 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
1702 return false;
1703 }
1704 if (!check_list_argument(term[1], check_rule_WhrDecl<atermpp::aterm>, 1))
1705 {
1706 mCRL2log(log::debug) << "check_rule_WhrDecl" << std::endl;
1707 return false;
1708 }
1709#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1710
1711#endif // MCRL2_NO_SOUNDNESS_CHECKS
1712 return true;
1713}
1714
1715// UntypedIdentifier(String)
1716template <typename Term>
1718{
1720#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1721 // check the type of the term
1722 const atermpp::aterm& term(t);
1723 if (!term.type_is_appl())
1724 {
1725 return false;
1726 }
1728 {
1729 return false;
1730 }
1731
1732 // check the children
1733 if (term.size() != 1)
1734 {
1735 return false;
1736 }
1737#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1738 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1739 {
1740 mCRL2log(log::debug) << "check_rule_String" << std::endl;
1741 return false;
1742 }
1743#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1744
1745#endif // MCRL2_NO_SOUNDNESS_CHECKS
1746 return true;
1747}
1748
1749// DataVarId(String, SortExpr)
1750template <typename Term>
1751bool check_term_DataVarId(const Term& t)
1752{
1754#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1755 // check the type of the term
1756 const atermpp::aterm& term(t);
1757 if (!term.type_is_appl())
1758 {
1759 return false;
1760 }
1762 {
1763 return false;
1764 }
1765
1766 // check the children
1767 if (term.size() != 2)
1768 {
1769 return false;
1770 }
1771#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1772 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1773 {
1774 mCRL2log(log::debug) << "check_rule_String" << std::endl;
1775 return false;
1776 }
1777 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1778 {
1779 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
1780 return false;
1781 }
1782#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1783
1784#endif // MCRL2_NO_SOUNDNESS_CHECKS
1785 return true;
1786}
1787
1788// OpId(String, SortExpr, Number)
1789template <typename Term>
1790bool check_term_OpId(const Term& t)
1791{
1793#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1794 // check the type of the term
1795 const atermpp::aterm& term(t);
1796 if (!term.type_is_appl())
1797 {
1798 return false;
1799 }
1801 {
1802 return false;
1803 }
1804
1805 // check the children
1806 if (term.size() != 3)
1807 {
1808 return false;
1809 }
1810#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1811 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1812 {
1813 mCRL2log(log::debug) << "check_rule_String" << std::endl;
1814 return false;
1815 }
1816 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
1817 {
1818 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
1819 return false;
1820 }
1821 if (!check_term_argument(term[2], check_rule_Number<atermpp::aterm>))
1822 {
1823 mCRL2log(log::debug) << "check_rule_Number" << std::endl;
1824 return false;
1825 }
1826#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1827
1828#endif // MCRL2_NO_SOUNDNESS_CHECKS
1829 return true;
1830}
1831
1832// UntypedDataParameter(String, DataExpr*)
1833template <typename Term>
1835{
1837#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1838 // check the type of the term
1839 const atermpp::aterm& term(t);
1840 if (!term.type_is_appl())
1841 {
1842 return false;
1843 }
1845 {
1846 return false;
1847 }
1848
1849 // check the children
1850 if (term.size() != 2)
1851 {
1852 return false;
1853 }
1854#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1855 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
1856 {
1857 mCRL2log(log::debug) << "check_rule_String" << std::endl;
1858 return false;
1859 }
1860 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
1861 {
1862 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
1863 return false;
1864 }
1865#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
1866
1867#endif // MCRL2_NO_SOUNDNESS_CHECKS
1868 return true;
1869}
1870
1871// Forall()
1872template <typename Term>
1873bool check_term_Forall(const Term& t)
1874{
1876#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1877 // check the type of the term
1878 const atermpp::aterm& term(t);
1879 if (!term.type_is_appl())
1880 {
1881 return false;
1882 }
1884 {
1885 return false;
1886 }
1887
1888 // check the children
1889 if (term.size() != 0)
1890 {
1891 return false;
1892 }
1893
1894#endif // MCRL2_NO_SOUNDNESS_CHECKS
1895 return true;
1896}
1897
1898// Exists()
1899template <typename Term>
1900bool check_term_Exists(const Term& t)
1901{
1903#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1904 // check the type of the term
1905 const atermpp::aterm& term(t);
1906 if (!term.type_is_appl())
1907 {
1908 return false;
1909 }
1911 {
1912 return false;
1913 }
1914
1915 // check the children
1916 if (term.size() != 0)
1917 {
1918 return false;
1919 }
1920
1921#endif // MCRL2_NO_SOUNDNESS_CHECKS
1922 return true;
1923}
1924
1925// SetComp()
1926template <typename Term>
1927bool check_term_SetComp(const Term& t)
1928{
1930#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1931 // check the type of the term
1932 const atermpp::aterm& term(t);
1933 if (!term.type_is_appl())
1934 {
1935 return false;
1936 }
1938 {
1939 return false;
1940 }
1941
1942 // check the children
1943 if (term.size() != 0)
1944 {
1945 return false;
1946 }
1947
1948#endif // MCRL2_NO_SOUNDNESS_CHECKS
1949 return true;
1950}
1951
1952// BagComp()
1953template <typename Term>
1954bool check_term_BagComp(const Term& t)
1955{
1957#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1958 // check the type of the term
1959 const atermpp::aterm& term(t);
1960 if (!term.type_is_appl())
1961 {
1962 return false;
1963 }
1965 {
1966 return false;
1967 }
1968
1969 // check the children
1970 if (term.size() != 0)
1971 {
1972 return false;
1973 }
1974
1975#endif // MCRL2_NO_SOUNDNESS_CHECKS
1976 return true;
1977}
1978
1979// Lambda()
1980template <typename Term>
1981bool check_term_Lambda(const Term& t)
1982{
1984#ifndef MCRL2_NO_SOUNDNESS_CHECKS
1985 // check the type of the term
1986 const atermpp::aterm& term(t);
1987 if (!term.type_is_appl())
1988 {
1989 return false;
1990 }
1992 {
1993 return false;
1994 }
1995
1996 // check the children
1997 if (term.size() != 0)
1998 {
1999 return false;
2000 }
2001
2002#endif // MCRL2_NO_SOUNDNESS_CHECKS
2003 return true;
2004}
2005
2006// UntypedSetBagComp()
2007template <typename Term>
2009{
2011#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2012 // check the type of the term
2013 const atermpp::aterm& term(t);
2014 if (!term.type_is_appl())
2015 {
2016 return false;
2017 }
2019 {
2020 return false;
2021 }
2022
2023 // check the children
2024 if (term.size() != 0)
2025 {
2026 return false;
2027 }
2028
2029#endif // MCRL2_NO_SOUNDNESS_CHECKS
2030 return true;
2031}
2032
2033// DataVarIdInit(DataVarId, DataExpr)
2034template <typename Term>
2035bool check_term_DataVarIdInit(const Term& t)
2036{
2038#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2039 // check the type of the term
2040 const atermpp::aterm& term(t);
2041 if (!term.type_is_appl())
2042 {
2043 return false;
2044 }
2046 {
2047 return false;
2048 }
2049
2050 // check the children
2051 if (term.size() != 2)
2052 {
2053 return false;
2054 }
2055#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2056 if (!check_term_argument(term[0], check_rule_DataVarId<atermpp::aterm>))
2057 {
2058 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
2059 return false;
2060 }
2061 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2062 {
2063 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
2064 return false;
2065 }
2066#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2067
2068#endif // MCRL2_NO_SOUNDNESS_CHECKS
2069 return true;
2070}
2071
2072// UntypedIdentifierAssignment(String, DataExpr)
2073template <typename Term>
2075{
2077#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2078 // check the type of the term
2079 const atermpp::aterm& term(t);
2080 if (!term.type_is_appl())
2081 {
2082 return false;
2083 }
2085 {
2086 return false;
2087 }
2088
2089 // check the children
2090 if (term.size() != 2)
2091 {
2092 return false;
2093 }
2094#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2095 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
2096 {
2097 mCRL2log(log::debug) << "check_rule_String" << std::endl;
2098 return false;
2099 }
2100 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2101 {
2102 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
2103 return false;
2104 }
2105#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2106
2107#endif // MCRL2_NO_SOUNDNESS_CHECKS
2108 return true;
2109}
2110
2111// DataSpec(SortSpec, ConsSpec, MapSpec, DataEqnSpec)
2112template <typename Term>
2113bool check_term_DataSpec(const Term& t)
2114{
2116#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2117 // check the type of the term
2118 const atermpp::aterm& term(t);
2119 if (!term.type_is_appl())
2120 {
2121 return false;
2122 }
2124 {
2125 return false;
2126 }
2127
2128 // check the children
2129 if (term.size() != 4)
2130 {
2131 return false;
2132 }
2133#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2134 if (!check_term_argument(term[0], check_rule_SortSpec<atermpp::aterm>))
2135 {
2136 mCRL2log(log::debug) << "check_rule_SortSpec" << std::endl;
2137 return false;
2138 }
2139 if (!check_term_argument(term[1], check_rule_ConsSpec<atermpp::aterm>))
2140 {
2141 mCRL2log(log::debug) << "check_rule_ConsSpec" << std::endl;
2142 return false;
2143 }
2144 if (!check_term_argument(term[2], check_rule_MapSpec<atermpp::aterm>))
2145 {
2146 mCRL2log(log::debug) << "check_rule_MapSpec" << std::endl;
2147 return false;
2148 }
2149 if (!check_term_argument(term[3], check_rule_DataEqnSpec<atermpp::aterm>))
2150 {
2151 mCRL2log(log::debug) << "check_rule_DataEqnSpec" << std::endl;
2152 return false;
2153 }
2154#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2155
2156#endif // MCRL2_NO_SOUNDNESS_CHECKS
2157 return true;
2158}
2159
2160// SortSpec(SortDecl*)
2161template <typename Term>
2162bool check_term_SortSpec(const Term& t)
2163{
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 }
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_SortDecl<atermpp::aterm>, 0))
2184 {
2185 mCRL2log(log::debug) << "check_rule_SortDecl" << 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// ConsSpec(OpId*)
2195template <typename Term>
2196bool check_term_ConsSpec(const Term& t)
2197{
2199#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2200 // check the type of the term
2201 const atermpp::aterm& term(t);
2202 if (!term.type_is_appl())
2203 {
2204 return false;
2205 }
2207 {
2208 return false;
2209 }
2210
2211 // check the children
2212 if (term.size() != 1)
2213 {
2214 return false;
2215 }
2216#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2217 if (!check_list_argument(term[0], check_rule_OpId<atermpp::aterm>, 0))
2218 {
2219 mCRL2log(log::debug) << "check_rule_OpId" << std::endl;
2220 return false;
2221 }
2222#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2223
2224#endif // MCRL2_NO_SOUNDNESS_CHECKS
2225 return true;
2226}
2227
2228// MapSpec(OpId*)
2229template <typename Term>
2230bool check_term_MapSpec(const Term& t)
2231{
2233#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2234 // check the type of the term
2235 const atermpp::aterm& term(t);
2236 if (!term.type_is_appl())
2237 {
2238 return false;
2239 }
2241 {
2242 return false;
2243 }
2244
2245 // check the children
2246 if (term.size() != 1)
2247 {
2248 return false;
2249 }
2250#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2251 if (!check_list_argument(term[0], check_rule_OpId<atermpp::aterm>, 0))
2252 {
2253 mCRL2log(log::debug) << "check_rule_OpId" << std::endl;
2254 return false;
2255 }
2256#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2257
2258#endif // MCRL2_NO_SOUNDNESS_CHECKS
2259 return true;
2260}
2261
2262// DataEqnSpec(DataEqn*)
2263template <typename Term>
2264bool check_term_DataEqnSpec(const Term& t)
2265{
2267#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2268 // check the type of the term
2269 const atermpp::aterm& term(t);
2270 if (!term.type_is_appl())
2271 {
2272 return false;
2273 }
2275 {
2276 return false;
2277 }
2278
2279 // check the children
2280 if (term.size() != 1)
2281 {
2282 return false;
2283 }
2284#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2285 if (!check_list_argument(term[0], check_rule_DataEqn<atermpp::aterm>, 0))
2286 {
2287 mCRL2log(log::debug) << "check_rule_DataEqn" << std::endl;
2288 return false;
2289 }
2290#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2291
2292#endif // MCRL2_NO_SOUNDNESS_CHECKS
2293 return true;
2294}
2295
2296// SortRef(SortId, SortExpr)
2297template <typename Term>
2298bool check_term_SortRef(const Term& t)
2299{
2301#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2302 // check the type of the term
2303 const atermpp::aterm& term(t);
2304 if (!term.type_is_appl())
2305 {
2306 return false;
2307 }
2309 {
2310 return false;
2311 }
2312
2313 // check the children
2314 if (term.size() != 2)
2315 {
2316 return false;
2317 }
2318#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2319 if (!check_term_argument(term[0], check_rule_SortId<atermpp::aterm>))
2320 {
2321 mCRL2log(log::debug) << "check_rule_SortId" << std::endl;
2322 return false;
2323 }
2324 if (!check_term_argument(term[1], check_rule_SortExpr<atermpp::aterm>))
2325 {
2326 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
2327 return false;
2328 }
2329#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2330
2331#endif // MCRL2_NO_SOUNDNESS_CHECKS
2332 return true;
2333}
2334
2335// DataEqn(DataVarId*, DataExpr, DataExpr, DataExpr)
2336template <typename Term>
2337bool check_term_DataEqn(const Term& t)
2338{
2340#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2341 // check the type of the term
2342 const atermpp::aterm& term(t);
2343 if (!term.type_is_appl())
2344 {
2345 return false;
2346 }
2348 {
2349 return false;
2350 }
2351
2352 // check the children
2353 if (term.size() != 4)
2354 {
2355 return false;
2356 }
2357#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2358 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
2359 {
2360 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
2361 return false;
2362 }
2363 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2364 {
2365 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
2366 return false;
2367 }
2368 if (!check_term_argument(term[2], check_rule_DataExpr<atermpp::aterm>))
2369 {
2370 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
2371 return false;
2372 }
2373 if (!check_term_argument(term[3], check_rule_DataExpr<atermpp::aterm>))
2374 {
2375 mCRL2log(log::debug) << "check_rule_DataExpr" << 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// MultAct(Action*)
2385template <typename Term>
2386bool check_term_MultAct(const Term& t)
2387{
2389#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2390 // check the type of the term
2391 const atermpp::aterm& term(t);
2392 if (!term.type_is_appl())
2393 {
2394 return false;
2395 }
2397 {
2398 return false;
2399 }
2400
2401 // check the children
2402 if (term.size() != 1)
2403 {
2404 return false;
2405 }
2406#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2407 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
2408 {
2409 mCRL2log(log::debug) << "check_rule_Action" << std::endl;
2410 return false;
2411 }
2412#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2413
2414#endif // MCRL2_NO_SOUNDNESS_CHECKS
2415 return true;
2416}
2417
2418// TimedMultAct(Action*, DataExpr)
2419template <typename Term>
2420bool check_term_TimedMultAct(const Term& t)
2421{
2423#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2424 // check the type of the term
2425 const atermpp::aterm& term(t);
2426 if (!term.type_is_appl())
2427 {
2428 return false;
2429 }
2431 {
2432 return false;
2433 }
2434
2435 // check the children
2436 if (term.size() != 2)
2437 {
2438 return false;
2439 }
2440#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2441 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
2442 {
2443 mCRL2log(log::debug) << "check_rule_Action" << std::endl;
2444 return false;
2445 }
2446 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
2447 {
2448 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
2449 return false;
2450 }
2451#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2452
2453#endif // MCRL2_NO_SOUNDNESS_CHECKS
2454 return true;
2455}
2456
2457// UntypedMultiAction(UntypedDataParameter*)
2458template <typename Term>
2460{
2462#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2463 // check the type of the term
2464 const atermpp::aterm& term(t);
2465 if (!term.type_is_appl())
2466 {
2467 return false;
2468 }
2470 {
2471 return false;
2472 }
2473
2474 // check the children
2475 if (term.size() != 1)
2476 {
2477 return false;
2478 }
2479#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2480 if (!check_list_argument(term[0], check_rule_UntypedDataParameter<atermpp::aterm>, 0))
2481 {
2482 mCRL2log(log::debug) << "check_rule_UntypedDataParameter" << std::endl;
2483 return false;
2484 }
2485#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2486
2487#endif // MCRL2_NO_SOUNDNESS_CHECKS
2488 return true;
2489}
2490
2491// Action(ActId, DataExpr*)
2492template <typename Term>
2493bool check_term_Action(const Term& t)
2494{
2496#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2497 // check the type of the term
2498 const atermpp::aterm& term(t);
2499 if (!term.type_is_appl())
2500 {
2501 return false;
2502 }
2504 {
2505 return false;
2506 }
2507
2508 // check the children
2509 if (term.size() != 2)
2510 {
2511 return false;
2512 }
2513#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2514 if (!check_term_argument(term[0], check_rule_ActId<atermpp::aterm>))
2515 {
2516 mCRL2log(log::debug) << "check_rule_ActId" << std::endl;
2517 return false;
2518 }
2519 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
2520 {
2521 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
2522 return false;
2523 }
2524#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2525
2526#endif // MCRL2_NO_SOUNDNESS_CHECKS
2527 return true;
2528}
2529
2530// ActId(String, SortExpr*)
2531template <typename Term>
2532bool check_term_ActId(const Term& t)
2533{
2535#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2536 // check the type of the term
2537 const atermpp::aterm& term(t);
2538 if (!term.type_is_appl())
2539 {
2540 return false;
2541 }
2543 {
2544 return false;
2545 }
2546
2547 // check the children
2548 if (term.size() != 2)
2549 {
2550 return false;
2551 }
2552#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2553 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
2554 {
2555 mCRL2log(log::debug) << "check_rule_String" << std::endl;
2556 return false;
2557 }
2558 if (!check_list_argument(term[1], check_rule_SortExpr<atermpp::aterm>, 0))
2559 {
2560 mCRL2log(log::debug) << "check_rule_SortExpr" << std::endl;
2561 return false;
2562 }
2563#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2564
2565#endif // MCRL2_NO_SOUNDNESS_CHECKS
2566 return true;
2567}
2568
2569// Process(ProcVarId, DataExpr*)
2570template <typename Term>
2571bool check_term_Process(const Term& t)
2572{
2574#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2575 // check the type of the term
2576 const atermpp::aterm& term(t);
2577 if (!term.type_is_appl())
2578 {
2579 return false;
2580 }
2582 {
2583 return false;
2584 }
2585
2586 // check the children
2587 if (term.size() != 2)
2588 {
2589 return false;
2590 }
2591#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2592 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
2593 {
2594 mCRL2log(log::debug) << "check_rule_ProcVarId" << std::endl;
2595 return false;
2596 }
2597 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
2598 {
2599 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
2600 return false;
2601 }
2602#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2603
2604#endif // MCRL2_NO_SOUNDNESS_CHECKS
2605 return true;
2606}
2607
2608// ProcessAssignment(ProcVarId, DataVarIdInit*)
2609template <typename Term>
2611{
2613#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2614 // check the type of the term
2615 const atermpp::aterm& term(t);
2616 if (!term.type_is_appl())
2617 {
2618 return false;
2619 }
2621 {
2622 return false;
2623 }
2624
2625 // check the children
2626 if (term.size() != 2)
2627 {
2628 return false;
2629 }
2630#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2631 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
2632 {
2633 mCRL2log(log::debug) << "check_rule_ProcVarId" << std::endl;
2634 return false;
2635 }
2636 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
2637 {
2638 mCRL2log(log::debug) << "check_rule_DataVarIdInit" << std::endl;
2639 return false;
2640 }
2641#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2642
2643#endif // MCRL2_NO_SOUNDNESS_CHECKS
2644 return true;
2645}
2646
2647// Delta()
2648template <typename Term>
2649bool check_term_Delta(const Term& t)
2650{
2652#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2653 // check the type of the term
2654 const atermpp::aterm& term(t);
2655 if (!term.type_is_appl())
2656 {
2657 return false;
2658 }
2660 {
2661 return false;
2662 }
2663
2664 // check the children
2665 if (term.size() != 0)
2666 {
2667 return false;
2668 }
2669
2670#endif // MCRL2_NO_SOUNDNESS_CHECKS
2671 return true;
2672}
2673
2674// Tau()
2675template <typename Term>
2676bool check_term_Tau(const Term& t)
2677{
2679#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2680 // check the type of the term
2681 const atermpp::aterm& term(t);
2682 if (!term.type_is_appl())
2683 {
2684 return false;
2685 }
2687 {
2688 return false;
2689 }
2690
2691 // check the children
2692 if (term.size() != 0)
2693 {
2694 return false;
2695 }
2696
2697#endif // MCRL2_NO_SOUNDNESS_CHECKS
2698 return true;
2699}
2700
2701// Sum(DataVarId+, ProcExpr)
2702template <typename Term>
2703bool check_term_Sum(const Term& t)
2704{
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 }
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_DataVarId<atermpp::aterm>, 1))
2725 {
2726 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
2727 return false;
2728 }
2729 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2730 {
2731 mCRL2log(log::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// Block(String*, ProcExpr)
2741template <typename Term>
2742bool check_term_Block(const Term& t)
2743{
2745#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2746 // check the type of the term
2747 const atermpp::aterm& term(t);
2748 if (!term.type_is_appl())
2749 {
2750 return false;
2751 }
2753 {
2754 return false;
2755 }
2756
2757 // check the children
2758 if (term.size() != 2)
2759 {
2760 return false;
2761 }
2762#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2763 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 0))
2764 {
2765 mCRL2log(log::debug) << "check_rule_String" << std::endl;
2766 return false;
2767 }
2768 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2769 {
2770 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
2771 return false;
2772 }
2773#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2774
2775#endif // MCRL2_NO_SOUNDNESS_CHECKS
2776 return true;
2777}
2778
2779// Hide(String*, ProcExpr)
2780template <typename Term>
2781bool check_term_Hide(const Term& t)
2782{
2784#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2785 // check the type of the term
2786 const atermpp::aterm& term(t);
2787 if (!term.type_is_appl())
2788 {
2789 return false;
2790 }
2792 {
2793 return false;
2794 }
2795
2796 // check the children
2797 if (term.size() != 2)
2798 {
2799 return false;
2800 }
2801#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2802 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 0))
2803 {
2804 mCRL2log(log::debug) << "check_rule_String" << std::endl;
2805 return false;
2806 }
2807 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2808 {
2809 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
2810 return false;
2811 }
2812#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2813
2814#endif // MCRL2_NO_SOUNDNESS_CHECKS
2815 return true;
2816}
2817
2818// Rename(RenameExpr*, ProcExpr)
2819template <typename Term>
2820bool check_term_Rename(const Term& t)
2821{
2823#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2824 // check the type of the term
2825 const atermpp::aterm& term(t);
2826 if (!term.type_is_appl())
2827 {
2828 return false;
2829 }
2831 {
2832 return false;
2833 }
2834
2835 // check the children
2836 if (term.size() != 2)
2837 {
2838 return false;
2839 }
2840#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2841 if (!check_list_argument(term[0], check_rule_RenameExpr<atermpp::aterm>, 0))
2842 {
2843 mCRL2log(log::debug) << "check_rule_RenameExpr" << std::endl;
2844 return false;
2845 }
2846 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2847 {
2848 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
2849 return false;
2850 }
2851#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2852
2853#endif // MCRL2_NO_SOUNDNESS_CHECKS
2854 return true;
2855}
2856
2857// Comm(CommExpr*, ProcExpr)
2858template <typename Term>
2859bool check_term_Comm(const Term& t)
2860{
2862#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2863 // check the type of the term
2864 const atermpp::aterm& term(t);
2865 if (!term.type_is_appl())
2866 {
2867 return false;
2868 }
2870 {
2871 return false;
2872 }
2873
2874 // check the children
2875 if (term.size() != 2)
2876 {
2877 return false;
2878 }
2879#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2880 if (!check_list_argument(term[0], check_rule_CommExpr<atermpp::aterm>, 0))
2881 {
2882 mCRL2log(log::debug) << "check_rule_CommExpr" << std::endl;
2883 return false;
2884 }
2885 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2886 {
2887 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
2888 return false;
2889 }
2890#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2891
2892#endif // MCRL2_NO_SOUNDNESS_CHECKS
2893 return true;
2894}
2895
2896// Allow(MultActName*, ProcExpr)
2897template <typename Term>
2898bool check_term_Allow(const Term& t)
2899{
2901#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2902 // check the type of the term
2903 const atermpp::aterm& term(t);
2904 if (!term.type_is_appl())
2905 {
2906 return false;
2907 }
2909 {
2910 return false;
2911 }
2912
2913 // check the children
2914 if (term.size() != 2)
2915 {
2916 return false;
2917 }
2918#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2919 if (!check_list_argument(term[0], check_rule_MultActName<atermpp::aterm>, 0))
2920 {
2921 mCRL2log(log::debug) << "check_rule_MultActName" << std::endl;
2922 return false;
2923 }
2924 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2925 {
2926 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
2927 return false;
2928 }
2929#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2930
2931#endif // MCRL2_NO_SOUNDNESS_CHECKS
2932 return true;
2933}
2934
2935// Sync(ProcExpr, ProcExpr)
2936template <typename Term>
2937bool check_term_Sync(const Term& t)
2938{
2940#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2941 // check the type of the term
2942 const atermpp::aterm& term(t);
2943 if (!term.type_is_appl())
2944 {
2945 return false;
2946 }
2948 {
2949 return false;
2950 }
2951
2952 // check the children
2953 if (term.size() != 2)
2954 {
2955 return false;
2956 }
2957#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2958 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2959 {
2960 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
2961 return false;
2962 }
2963 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
2964 {
2965 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
2966 return false;
2967 }
2968#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2969
2970#endif // MCRL2_NO_SOUNDNESS_CHECKS
2971 return true;
2972}
2973
2974// AtTime(ProcExpr, DataExpr)
2975template <typename Term>
2976bool check_term_AtTime(const Term& t)
2977{
2979#ifndef MCRL2_NO_SOUNDNESS_CHECKS
2980 // check the type of the term
2981 const atermpp::aterm& term(t);
2982 if (!term.type_is_appl())
2983 {
2984 return false;
2985 }
2987 {
2988 return false;
2989 }
2990
2991 // check the children
2992 if (term.size() != 2)
2993 {
2994 return false;
2995 }
2996#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
2997 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
2998 {
2999 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3000 return false;
3001 }
3002 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3003 {
3004 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3005 return false;
3006 }
3007#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3008
3009#endif // MCRL2_NO_SOUNDNESS_CHECKS
3010 return true;
3011}
3012
3013// Seq(ProcExpr, ProcExpr)
3014template <typename Term>
3015bool check_term_Seq(const Term& t)
3016{
3018#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3019 // check the type of the term
3020 const atermpp::aterm& term(t);
3021 if (!term.type_is_appl())
3022 {
3023 return false;
3024 }
3026 {
3027 return false;
3028 }
3029
3030 // check the children
3031 if (term.size() != 2)
3032 {
3033 return false;
3034 }
3035#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3036 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3037 {
3038 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3039 return false;
3040 }
3041 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3042 {
3043 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3044 return false;
3045 }
3046#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3047
3048#endif // MCRL2_NO_SOUNDNESS_CHECKS
3049 return true;
3050}
3051
3052// IfThen(DataExpr, ProcExpr)
3053template <typename Term>
3054bool check_term_IfThen(const Term& t)
3055{
3057#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3058 // check the type of the term
3059 const atermpp::aterm& term(t);
3060 if (!term.type_is_appl())
3061 {
3062 return false;
3063 }
3065 {
3066 return false;
3067 }
3068
3069 // check the children
3070 if (term.size() != 2)
3071 {
3072 return false;
3073 }
3074#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3075 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
3076 {
3077 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3078 return false;
3079 }
3080 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3081 {
3082 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3083 return false;
3084 }
3085#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3086
3087#endif // MCRL2_NO_SOUNDNESS_CHECKS
3088 return true;
3089}
3090
3091// IfThenElse(DataExpr, ProcExpr, ProcExpr)
3092template <typename Term>
3093bool check_term_IfThenElse(const Term& t)
3094{
3096#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3097 // check the type of the term
3098 const atermpp::aterm& term(t);
3099 if (!term.type_is_appl())
3100 {
3101 return false;
3102 }
3104 {
3105 return false;
3106 }
3107
3108 // check the children
3109 if (term.size() != 3)
3110 {
3111 return false;
3112 }
3113#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3114 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
3115 {
3116 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3117 return false;
3118 }
3119 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3120 {
3121 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3122 return false;
3123 }
3124 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3125 {
3126 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3127 return false;
3128 }
3129#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3130
3131#endif // MCRL2_NO_SOUNDNESS_CHECKS
3132 return true;
3133}
3134
3135// BInit(ProcExpr, ProcExpr)
3136template <typename Term>
3137bool check_term_BInit(const Term& t)
3138{
3140#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3141 // check the type of the term
3142 const atermpp::aterm& term(t);
3143 if (!term.type_is_appl())
3144 {
3145 return false;
3146 }
3148 {
3149 return false;
3150 }
3151
3152 // check the children
3153 if (term.size() != 2)
3154 {
3155 return false;
3156 }
3157#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3158 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3159 {
3160 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3161 return false;
3162 }
3163 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3164 {
3165 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3166 return false;
3167 }
3168#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3169
3170#endif // MCRL2_NO_SOUNDNESS_CHECKS
3171 return true;
3172}
3173
3174// Merge(ProcExpr, ProcExpr)
3175template <typename Term>
3176bool check_term_Merge(const Term& t)
3177{
3179#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3180 // check the type of the term
3181 const atermpp::aterm& term(t);
3182 if (!term.type_is_appl())
3183 {
3184 return false;
3185 }
3187 {
3188 return false;
3189 }
3190
3191 // check the children
3192 if (term.size() != 2)
3193 {
3194 return false;
3195 }
3196#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3197 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3198 {
3199 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3200 return false;
3201 }
3202 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3203 {
3204 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3205 return false;
3206 }
3207#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3208
3209#endif // MCRL2_NO_SOUNDNESS_CHECKS
3210 return true;
3211}
3212
3213// LMerge(ProcExpr, ProcExpr)
3214template <typename Term>
3215bool check_term_LMerge(const Term& t)
3216{
3218#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3219 // check the type of the term
3220 const atermpp::aterm& term(t);
3221 if (!term.type_is_appl())
3222 {
3223 return false;
3224 }
3226 {
3227 return false;
3228 }
3229
3230 // check the children
3231 if (term.size() != 2)
3232 {
3233 return false;
3234 }
3235#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3236 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3237 {
3238 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3239 return false;
3240 }
3241 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3242 {
3243 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3244 return false;
3245 }
3246#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3247
3248#endif // MCRL2_NO_SOUNDNESS_CHECKS
3249 return true;
3250}
3251
3252// Choice(ProcExpr, ProcExpr)
3253template <typename Term>
3254bool check_term_Choice(const Term& t)
3255{
3257#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3258 // check the type of the term
3259 const atermpp::aterm& term(t);
3260 if (!term.type_is_appl())
3261 {
3262 return false;
3263 }
3265 {
3266 return false;
3267 }
3268
3269 // check the children
3270 if (term.size() != 2)
3271 {
3272 return false;
3273 }
3274#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3275 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3276 {
3277 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3278 return false;
3279 }
3280 if (!check_term_argument(term[1], check_rule_ProcExpr<atermpp::aterm>))
3281 {
3282 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3283 return false;
3284 }
3285#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3286
3287#endif // MCRL2_NO_SOUNDNESS_CHECKS
3288 return true;
3289}
3290
3291// StochasticOperator(DataVarId+, DataExpr, ProcExpr)
3292template <typename Term>
3294{
3296#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3297 // check the type of the term
3298 const atermpp::aterm& term(t);
3299 if (!term.type_is_appl())
3300 {
3301 return false;
3302 }
3304 {
3305 return false;
3306 }
3307
3308 // check the children
3309 if (term.size() != 3)
3310 {
3311 return false;
3312 }
3313#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3314 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
3315 {
3316 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
3317 return false;
3318 }
3319 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3320 {
3321 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3322 return false;
3323 }
3324 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3325 {
3326 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3327 return false;
3328 }
3329#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3330
3331#endif // MCRL2_NO_SOUNDNESS_CHECKS
3332 return true;
3333}
3334
3335// UntypedProcessAssignment(String, UntypedIdentifierAssignment*)
3336template <typename Term>
3338{
3340#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3341 // check the type of the term
3342 const atermpp::aterm& term(t);
3343 if (!term.type_is_appl())
3344 {
3345 return false;
3346 }
3348 {
3349 return false;
3350 }
3351
3352 // check the children
3353 if (term.size() != 2)
3354 {
3355 return false;
3356 }
3357#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3358 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3359 {
3360 mCRL2log(log::debug) << "check_rule_String" << std::endl;
3361 return false;
3362 }
3363 if (!check_list_argument(term[1], check_rule_UntypedIdentifierAssignment<atermpp::aterm>, 0))
3364 {
3365 mCRL2log(log::debug) << "check_rule_UntypedIdentifierAssignment" << std::endl;
3366 return false;
3367 }
3368#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3369
3370#endif // MCRL2_NO_SOUNDNESS_CHECKS
3371 return true;
3372}
3373
3374// ProcVarId(String, DataVarId*)
3375template <typename Term>
3376bool check_term_ProcVarId(const Term& t)
3377{
3379#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3380 // check the type of the term
3381 const atermpp::aterm& term(t);
3382 if (!term.type_is_appl())
3383 {
3384 return false;
3385 }
3387 {
3388 return false;
3389 }
3390
3391 // check the children
3392 if (term.size() != 2)
3393 {
3394 return false;
3395 }
3396#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3397 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3398 {
3399 mCRL2log(log::debug) << "check_rule_String" << std::endl;
3400 return false;
3401 }
3402 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
3403 {
3404 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
3405 return false;
3406 }
3407#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3408
3409#endif // MCRL2_NO_SOUNDNESS_CHECKS
3410 return true;
3411}
3412
3413// MultActName(String+)
3414template <typename Term>
3415bool check_term_MultActName(const Term& t)
3416{
3418#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3419 // check the type of the term
3420 const atermpp::aterm& term(t);
3421 if (!term.type_is_appl())
3422 {
3423 return false;
3424 }
3426 {
3427 return false;
3428 }
3429
3430 // check the children
3431 if (term.size() != 1)
3432 {
3433 return false;
3434 }
3435#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3436 if (!check_list_argument(term[0], check_rule_String<atermpp::aterm>, 1))
3437 {
3438 mCRL2log(log::debug) << "check_rule_String" << std::endl;
3439 return false;
3440 }
3441#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3442
3443#endif // MCRL2_NO_SOUNDNESS_CHECKS
3444 return true;
3445}
3446
3447// RenameExpr(String, String)
3448template <typename Term>
3449bool check_term_RenameExpr(const Term& t)
3450{
3452#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3453 // check the type of the term
3454 const atermpp::aterm& term(t);
3455 if (!term.type_is_appl())
3456 {
3457 return false;
3458 }
3460 {
3461 return false;
3462 }
3463
3464 // check the children
3465 if (term.size() != 2)
3466 {
3467 return false;
3468 }
3469#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3470 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
3471 {
3472 mCRL2log(log::debug) << "check_rule_String" << std::endl;
3473 return false;
3474 }
3475 if (!check_term_argument(term[1], check_rule_String<atermpp::aterm>))
3476 {
3477 mCRL2log(log::debug) << "check_rule_String" << std::endl;
3478 return false;
3479 }
3480#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3481
3482#endif // MCRL2_NO_SOUNDNESS_CHECKS
3483 return true;
3484}
3485
3486// CommExpr(MultActName, String)
3487template <typename Term>
3488bool check_term_CommExpr(const Term& t)
3489{
3491#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3492 // check the type of the term
3493 const atermpp::aterm& term(t);
3494 if (!term.type_is_appl())
3495 {
3496 return false;
3497 }
3499 {
3500 return false;
3501 }
3502
3503 // check the children
3504 if (term.size() != 2)
3505 {
3506 return false;
3507 }
3508#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3509 if (!check_term_argument(term[0], check_rule_MultActName<atermpp::aterm>))
3510 {
3511 mCRL2log(log::debug) << "check_rule_MultActName" << std::endl;
3512 return false;
3513 }
3514 if (!check_term_argument(term[1], check_rule_String<atermpp::aterm>))
3515 {
3516 mCRL2log(log::debug) << "check_rule_String" << std::endl;
3517 return false;
3518 }
3519#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3520
3521#endif // MCRL2_NO_SOUNDNESS_CHECKS
3522 return true;
3523}
3524
3525// ProcSpec(DataSpec, ActSpec, GlobVarSpec, ProcEqnSpec, ProcInit)
3526template <typename Term>
3527bool check_term_ProcSpec(const Term& t)
3528{
3530#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3531 // check the type of the term
3532 const atermpp::aterm& term(t);
3533 if (!term.type_is_appl())
3534 {
3535 return false;
3536 }
3538 {
3539 return false;
3540 }
3541
3542 // check the children
3543 if (term.size() != 5)
3544 {
3545 return false;
3546 }
3547#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3548 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
3549 {
3550 mCRL2log(log::debug) << "check_rule_DataSpec" << std::endl;
3551 return false;
3552 }
3553 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
3554 {
3555 mCRL2log(log::debug) << "check_rule_ActSpec" << std::endl;
3556 return false;
3557 }
3558 if (!check_term_argument(term[2], check_rule_GlobVarSpec<atermpp::aterm>))
3559 {
3560 mCRL2log(log::debug) << "check_rule_GlobVarSpec" << std::endl;
3561 return false;
3562 }
3563 if (!check_term_argument(term[3], check_rule_ProcEqnSpec<atermpp::aterm>))
3564 {
3565 mCRL2log(log::debug) << "check_rule_ProcEqnSpec" << std::endl;
3566 return false;
3567 }
3568 if (!check_term_argument(term[4], check_rule_ProcInit<atermpp::aterm>))
3569 {
3570 mCRL2log(log::debug) << "check_rule_ProcInit" << std::endl;
3571 return false;
3572 }
3573#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3574
3575#endif // MCRL2_NO_SOUNDNESS_CHECKS
3576 return true;
3577}
3578
3579// ActSpec(ActId*)
3580template <typename Term>
3581bool check_term_ActSpec(const Term& t)
3582{
3584#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3585 // check the type of the term
3586 const atermpp::aterm& term(t);
3587 if (!term.type_is_appl())
3588 {
3589 return false;
3590 }
3592 {
3593 return false;
3594 }
3595
3596 // check the children
3597 if (term.size() != 1)
3598 {
3599 return false;
3600 }
3601#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3602 if (!check_list_argument(term[0], check_rule_ActId<atermpp::aterm>, 0))
3603 {
3604 mCRL2log(log::debug) << "check_rule_ActId" << std::endl;
3605 return false;
3606 }
3607#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3608
3609#endif // MCRL2_NO_SOUNDNESS_CHECKS
3610 return true;
3611}
3612
3613// GlobVarSpec(DataVarId*)
3614template <typename Term>
3615bool check_term_GlobVarSpec(const Term& t)
3616{
3618#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3619 // check the type of the term
3620 const atermpp::aterm& term(t);
3621 if (!term.type_is_appl())
3622 {
3623 return false;
3624 }
3626 {
3627 return false;
3628 }
3629
3630 // check the children
3631 if (term.size() != 1)
3632 {
3633 return false;
3634 }
3635#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3636 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3637 {
3638 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
3639 return false;
3640 }
3641#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3642
3643#endif // MCRL2_NO_SOUNDNESS_CHECKS
3644 return true;
3645}
3646
3647// ProcEqnSpec(ProcEqn*)
3648template <typename Term>
3649bool check_term_ProcEqnSpec(const Term& t)
3650{
3652#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3653 // check the type of the term
3654 const atermpp::aterm& term(t);
3655 if (!term.type_is_appl())
3656 {
3657 return false;
3658 }
3660 {
3661 return false;
3662 }
3663
3664 // check the children
3665 if (term.size() != 1)
3666 {
3667 return false;
3668 }
3669#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3670 if (!check_list_argument(term[0], check_rule_ProcEqn<atermpp::aterm>, 0))
3671 {
3672 mCRL2log(log::debug) << "check_rule_ProcEqn" << std::endl;
3673 return false;
3674 }
3675#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3676
3677#endif // MCRL2_NO_SOUNDNESS_CHECKS
3678 return true;
3679}
3680
3681// ProcEqn(ProcVarId, DataVarId*, ProcExpr)
3682template <typename Term>
3683bool check_term_ProcEqn(const Term& t)
3684{
3686#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3687 // check the type of the term
3688 const atermpp::aterm& term(t);
3689 if (!term.type_is_appl())
3690 {
3691 return false;
3692 }
3694 {
3695 return false;
3696 }
3697
3698 // check the children
3699 if (term.size() != 3)
3700 {
3701 return false;
3702 }
3703#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3704 if (!check_term_argument(term[0], check_rule_ProcVarId<atermpp::aterm>))
3705 {
3706 mCRL2log(log::debug) << "check_rule_ProcVarId" << std::endl;
3707 return false;
3708 }
3709 if (!check_list_argument(term[1], check_rule_DataVarId<atermpp::aterm>, 0))
3710 {
3711 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
3712 return false;
3713 }
3714 if (!check_term_argument(term[2], check_rule_ProcExpr<atermpp::aterm>))
3715 {
3716 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3717 return false;
3718 }
3719#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3720
3721#endif // MCRL2_NO_SOUNDNESS_CHECKS
3722 return true;
3723}
3724
3725// ProcessInit(ProcExpr)
3726template <typename Term>
3727bool check_term_ProcessInit(const Term& t)
3728{
3730#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3731 // check the type of the term
3732 const atermpp::aterm& term(t);
3733 if (!term.type_is_appl())
3734 {
3735 return false;
3736 }
3738 {
3739 return false;
3740 }
3741
3742 // check the children
3743 if (term.size() != 1)
3744 {
3745 return false;
3746 }
3747#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3748 if (!check_term_argument(term[0], check_rule_ProcExpr<atermpp::aterm>))
3749 {
3750 mCRL2log(log::debug) << "check_rule_ProcExpr" << std::endl;
3751 return false;
3752 }
3753#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3754
3755#endif // MCRL2_NO_SOUNDNESS_CHECKS
3756 return true;
3757}
3758
3759// Distribution(DataVarId*, DataExpr)
3760template <typename Term>
3761bool check_term_Distribution(const Term& t)
3762{
3764#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3765 // check the type of the term
3766 const atermpp::aterm& term(t);
3767 if (!term.type_is_appl())
3768 {
3769 return false;
3770 }
3772 {
3773 return false;
3774 }
3775
3776 // check the children
3777 if (term.size() != 2)
3778 {
3779 return false;
3780 }
3781#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3782 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3783 {
3784 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
3785 return false;
3786 }
3787 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3788 {
3789 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3790 return false;
3791 }
3792#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3793
3794#endif // MCRL2_NO_SOUNDNESS_CHECKS
3795 return true;
3796}
3797
3798// LinProcSpec(DataSpec, ActSpec, GlobVarSpec, LinearProcess, LinearProcessInit)
3799template <typename Term>
3800bool check_term_LinProcSpec(const Term& t)
3801{
3803#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3804 // check the type of the term
3805 const atermpp::aterm& term(t);
3806 if (!term.type_is_appl())
3807 {
3808 return false;
3809 }
3811 {
3812 return false;
3813 }
3814
3815 // check the children
3816 if (term.size() != 5)
3817 {
3818 return false;
3819 }
3820#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3821 if (!check_term_argument(term[0], check_rule_DataSpec<atermpp::aterm>))
3822 {
3823 mCRL2log(log::debug) << "check_rule_DataSpec" << std::endl;
3824 return false;
3825 }
3826 if (!check_term_argument(term[1], check_rule_ActSpec<atermpp::aterm>))
3827 {
3828 mCRL2log(log::debug) << "check_rule_ActSpec" << std::endl;
3829 return false;
3830 }
3831 if (!check_term_argument(term[2], check_rule_GlobVarSpec<atermpp::aterm>))
3832 {
3833 mCRL2log(log::debug) << "check_rule_GlobVarSpec" << std::endl;
3834 return false;
3835 }
3836 if (!check_term_argument(term[3], check_rule_LinearProcess<atermpp::aterm>))
3837 {
3838 mCRL2log(log::debug) << "check_rule_LinearProcess" << std::endl;
3839 return false;
3840 }
3841 if (!check_term_argument(term[4], check_rule_LinearProcessInit<atermpp::aterm>))
3842 {
3843 mCRL2log(log::debug) << "check_rule_LinearProcessInit" << std::endl;
3844 return false;
3845 }
3846#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3847
3848#endif // MCRL2_NO_SOUNDNESS_CHECKS
3849 return true;
3850}
3851
3852// LinearProcess(DataVarId*, LinearProcessSummand*)
3853template <typename Term>
3854bool check_term_LinearProcess(const Term& t)
3855{
3857#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3858 // check the type of the term
3859 const atermpp::aterm& term(t);
3860 if (!term.type_is_appl())
3861 {
3862 return false;
3863 }
3865 {
3866 return false;
3867 }
3868
3869 // check the children
3870 if (term.size() != 2)
3871 {
3872 return false;
3873 }
3874#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3875 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3876 {
3877 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
3878 return false;
3879 }
3880 if (!check_list_argument(term[1], check_rule_LinearProcessSummand<atermpp::aterm>, 0))
3881 {
3882 mCRL2log(log::debug) << "check_rule_LinearProcessSummand" << std::endl;
3883 return false;
3884 }
3885#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3886
3887#endif // MCRL2_NO_SOUNDNESS_CHECKS
3888 return true;
3889}
3890
3891// LinearProcessSummand(DataVarId*, DataExpr, MultActOrDelta, DataExpr, DataVarIdInit*, Distribution)
3892template <typename Term>
3894{
3896#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3897 // check the type of the term
3898 const atermpp::aterm& term(t);
3899 if (!term.type_is_appl())
3900 {
3901 return false;
3902 }
3904 {
3905 return false;
3906 }
3907
3908 // check the children
3909 if (term.size() != 6)
3910 {
3911 return false;
3912 }
3913#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3914 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
3915 {
3916 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
3917 return false;
3918 }
3919 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
3920 {
3921 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3922 return false;
3923 }
3924 if (!check_term_argument(term[2], check_rule_MultActOrDelta<atermpp::aterm>))
3925 {
3926 mCRL2log(log::debug) << "check_rule_MultActOrDelta" << std::endl;
3927 return false;
3928 }
3929 if (!check_term_argument(term[3], check_rule_DataExpr<atermpp::aterm>))
3930 {
3931 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3932 return false;
3933 }
3934 if (!check_list_argument(term[4], check_rule_DataVarIdInit<atermpp::aterm>, 0))
3935 {
3936 mCRL2log(log::debug) << "check_rule_DataVarIdInit" << std::endl;
3937 return false;
3938 }
3939 if (!check_term_argument(term[5], check_rule_Distribution<atermpp::aterm>))
3940 {
3941 mCRL2log(log::debug) << "check_rule_Distribution" << std::endl;
3942 return false;
3943 }
3944#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3945
3946#endif // MCRL2_NO_SOUNDNESS_CHECKS
3947 return true;
3948}
3949
3950// LinearProcessInit(DataExpr*, Distribution)
3951template <typename Term>
3953{
3955#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3956 // check the type of the term
3957 const atermpp::aterm& term(t);
3958 if (!term.type_is_appl())
3959 {
3960 return false;
3961 }
3963 {
3964 return false;
3965 }
3966
3967 // check the children
3968 if (term.size() != 2)
3969 {
3970 return false;
3971 }
3972#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3973 if (!check_list_argument(term[0], check_rule_DataExpr<atermpp::aterm>, 0))
3974 {
3975 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
3976 return false;
3977 }
3978 if (!check_term_argument(term[1], check_rule_Distribution<atermpp::aterm>))
3979 {
3980 mCRL2log(log::debug) << "check_rule_Distribution" << std::endl;
3981 return false;
3982 }
3983#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
3984
3985#endif // MCRL2_NO_SOUNDNESS_CHECKS
3986 return true;
3987}
3988
3989// StateTrue()
3990template <typename Term>
3991bool check_term_StateTrue(const Term& t)
3992{
3994#ifndef MCRL2_NO_SOUNDNESS_CHECKS
3995 // check the type of the term
3996 const atermpp::aterm& term(t);
3997 if (!term.type_is_appl())
3998 {
3999 return false;
4000 }
4002 {
4003 return false;
4004 }
4005
4006 // check the children
4007 if (term.size() != 0)
4008 {
4009 return false;
4010 }
4011
4012#endif // MCRL2_NO_SOUNDNESS_CHECKS
4013 return true;
4014}
4015
4016// StateFalse()
4017template <typename Term>
4018bool check_term_StateFalse(const Term& t)
4019{
4021#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4022 // check the type of the term
4023 const atermpp::aterm& term(t);
4024 if (!term.type_is_appl())
4025 {
4026 return false;
4027 }
4029 {
4030 return false;
4031 }
4032
4033 // check the children
4034 if (term.size() != 0)
4035 {
4036 return false;
4037 }
4038
4039#endif // MCRL2_NO_SOUNDNESS_CHECKS
4040 return true;
4041}
4042
4043// StateNot(StateFrm)
4044template <typename Term>
4045bool check_term_StateNot(const Term& t)
4046{
4048#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4049 // check the type of the term
4050 const atermpp::aterm& term(t);
4051 if (!term.type_is_appl())
4052 {
4053 return false;
4054 }
4056 {
4057 return false;
4058 }
4059
4060 // check the children
4061 if (term.size() != 1)
4062 {
4063 return false;
4064 }
4065#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4066 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4067 {
4068 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4069 return false;
4070 }
4071#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4072
4073#endif // MCRL2_NO_SOUNDNESS_CHECKS
4074 return true;
4075}
4076
4077// StateMinus(StateFrm)
4078template <typename Term>
4079bool check_term_StateMinus(const Term& t)
4080{
4082#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4083 // check the type of the term
4084 const atermpp::aterm& term(t);
4085 if (!term.type_is_appl())
4086 {
4087 return false;
4088 }
4090 {
4091 return false;
4092 }
4093
4094 // check the children
4095 if (term.size() != 1)
4096 {
4097 return false;
4098 }
4099#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4100 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4101 {
4102 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4103 return false;
4104 }
4105#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4106
4107#endif // MCRL2_NO_SOUNDNESS_CHECKS
4108 return true;
4109}
4110
4111// StateAnd(StateFrm, StateFrm)
4112template <typename Term>
4113bool check_term_StateAnd(const Term& t)
4114{
4116#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4117 // check the type of the term
4118 const atermpp::aterm& term(t);
4119 if (!term.type_is_appl())
4120 {
4121 return false;
4122 }
4124 {
4125 return false;
4126 }
4127
4128 // check the children
4129 if (term.size() != 2)
4130 {
4131 return false;
4132 }
4133#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4134 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4135 {
4136 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4137 return false;
4138 }
4139 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4140 {
4141 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4142 return false;
4143 }
4144#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4145
4146#endif // MCRL2_NO_SOUNDNESS_CHECKS
4147 return true;
4148}
4149
4150// StateOr(StateFrm, StateFrm)
4151template <typename Term>
4152bool check_term_StateOr(const Term& t)
4153{
4155#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4156 // check the type of the term
4157 const atermpp::aterm& term(t);
4158 if (!term.type_is_appl())
4159 {
4160 return false;
4161 }
4163 {
4164 return false;
4165 }
4166
4167 // check the children
4168 if (term.size() != 2)
4169 {
4170 return false;
4171 }
4172#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4173 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4174 {
4175 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4176 return false;
4177 }
4178 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4179 {
4180 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4181 return false;
4182 }
4183#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4184
4185#endif // MCRL2_NO_SOUNDNESS_CHECKS
4186 return true;
4187}
4188
4189// StateImp(StateFrm, StateFrm)
4190template <typename Term>
4191bool check_term_StateImp(const Term& t)
4192{
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 }
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_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4213 {
4214 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4215 return false;
4216 }
4217 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4218 {
4219 mCRL2log(log::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// StatePlus(StateFrm, StateFrm)
4229template <typename Term>
4230bool check_term_StatePlus(const Term& t)
4231{
4233#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4234 // check the type of the term
4235 const atermpp::aterm& term(t);
4236 if (!term.type_is_appl())
4237 {
4238 return false;
4239 }
4241 {
4242 return false;
4243 }
4244
4245 // check the children
4246 if (term.size() != 2)
4247 {
4248 return false;
4249 }
4250#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4251 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4252 {
4253 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4254 return false;
4255 }
4256 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4257 {
4258 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4259 return false;
4260 }
4261#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4262
4263#endif // MCRL2_NO_SOUNDNESS_CHECKS
4264 return true;
4265}
4266
4267// StateConstantMultiply(DataExpr, StateFrm)
4268template <typename Term>
4270{
4272#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4273 // check the type of the term
4274 const atermpp::aterm& term(t);
4275 if (!term.type_is_appl())
4276 {
4277 return false;
4278 }
4280 {
4281 return false;
4282 }
4283
4284 // check the children
4285 if (term.size() != 2)
4286 {
4287 return false;
4288 }
4289#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4290 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4291 {
4292 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
4293 return false;
4294 }
4295 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4296 {
4297 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4298 return false;
4299 }
4300#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4301
4302#endif // MCRL2_NO_SOUNDNESS_CHECKS
4303 return true;
4304}
4305
4306// StateConstantMultiplyAlt(StateFrm, DataExpr)
4307template <typename Term>
4309{
4311#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4312 // check the type of the term
4313 const atermpp::aterm& term(t);
4314 if (!term.type_is_appl())
4315 {
4316 return false;
4317 }
4319 {
4320 return false;
4321 }
4322
4323 // check the children
4324 if (term.size() != 2)
4325 {
4326 return false;
4327 }
4328#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4329 if (!check_term_argument(term[0], check_rule_StateFrm<atermpp::aterm>))
4330 {
4331 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4332 return false;
4333 }
4334 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
4335 {
4336 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
4337 return false;
4338 }
4339#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4340
4341#endif // MCRL2_NO_SOUNDNESS_CHECKS
4342 return true;
4343}
4344
4345// StateForall(DataVarId+, StateFrm)
4346template <typename Term>
4347bool check_term_StateForall(const Term& t)
4348{
4350#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4351 // check the type of the term
4352 const atermpp::aterm& term(t);
4353 if (!term.type_is_appl())
4354 {
4355 return false;
4356 }
4358 {
4359 return false;
4360 }
4361
4362 // check the children
4363 if (term.size() != 2)
4364 {
4365 return false;
4366 }
4367#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4368 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4369 {
4370 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
4371 return false;
4372 }
4373 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4374 {
4375 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4376 return false;
4377 }
4378#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4379
4380#endif // MCRL2_NO_SOUNDNESS_CHECKS
4381 return true;
4382}
4383
4384// StateExists(DataVarId+, StateFrm)
4385template <typename Term>
4386bool check_term_StateExists(const Term& t)
4387{
4389#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4390 // check the type of the term
4391 const atermpp::aterm& term(t);
4392 if (!term.type_is_appl())
4393 {
4394 return false;
4395 }
4397 {
4398 return false;
4399 }
4400
4401 // check the children
4402 if (term.size() != 2)
4403 {
4404 return false;
4405 }
4406#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4407 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4408 {
4409 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
4410 return false;
4411 }
4412 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4413 {
4414 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4415 return false;
4416 }
4417#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4418
4419#endif // MCRL2_NO_SOUNDNESS_CHECKS
4420 return true;
4421}
4422
4423// StateInfimum(DataVarId+, StateFrm)
4424template <typename Term>
4425bool check_term_StateInfimum(const Term& t)
4426{
4428#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4429 // check the type of the term
4430 const atermpp::aterm& term(t);
4431 if (!term.type_is_appl())
4432 {
4433 return false;
4434 }
4436 {
4437 return false;
4438 }
4439
4440 // check the children
4441 if (term.size() != 2)
4442 {
4443 return false;
4444 }
4445#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4446 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4447 {
4448 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
4449 return false;
4450 }
4451 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4452 {
4453 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4454 return false;
4455 }
4456#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4457
4458#endif // MCRL2_NO_SOUNDNESS_CHECKS
4459 return true;
4460}
4461
4462// StateSupremum(DataVarId+, StateFrm)
4463template <typename Term>
4464bool check_term_StateSupremum(const Term& t)
4465{
4467#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4468 // check the type of the term
4469 const atermpp::aterm& term(t);
4470 if (!term.type_is_appl())
4471 {
4472 return false;
4473 }
4475 {
4476 return false;
4477 }
4478
4479 // check the children
4480 if (term.size() != 2)
4481 {
4482 return false;
4483 }
4484#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4485 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4486 {
4487 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
4488 return false;
4489 }
4490 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4491 {
4492 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4493 return false;
4494 }
4495#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4496
4497#endif // MCRL2_NO_SOUNDNESS_CHECKS
4498 return true;
4499}
4500
4501// StateSum(DataVarId+, StateFrm)
4502template <typename Term>
4503bool check_term_StateSum(const Term& t)
4504{
4506#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4507 // check the type of the term
4508 const atermpp::aterm& term(t);
4509 if (!term.type_is_appl())
4510 {
4511 return false;
4512 }
4514 {
4515 return false;
4516 }
4517
4518 // check the children
4519 if (term.size() != 2)
4520 {
4521 return false;
4522 }
4523#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4524 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
4525 {
4526 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
4527 return false;
4528 }
4529 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4530 {
4531 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4532 return false;
4533 }
4534#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4535
4536#endif // MCRL2_NO_SOUNDNESS_CHECKS
4537 return true;
4538}
4539
4540// StateMust(RegFrm, StateFrm)
4541template <typename Term>
4542bool check_term_StateMust(const Term& t)
4543{
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 }
4553 {
4554 return false;
4555 }
4556
4557 // check the children
4558 if (term.size() != 2)
4559 {
4560 return false;
4561 }
4562#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4563 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4564 {
4565 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
4566 return false;
4567 }
4568 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4569 {
4570 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4571 return false;
4572 }
4573#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4574
4575#endif // MCRL2_NO_SOUNDNESS_CHECKS
4576 return true;
4577}
4578
4579// StateMay(RegFrm, StateFrm)
4580template <typename Term>
4581bool check_term_StateMay(const Term& t)
4582{
4584#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4585 // check the type of the term
4586 const atermpp::aterm& term(t);
4587 if (!term.type_is_appl())
4588 {
4589 return false;
4590 }
4592 {
4593 return false;
4594 }
4595
4596 // check the children
4597 if (term.size() != 2)
4598 {
4599 return false;
4600 }
4601#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4602 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4603 {
4604 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
4605 return false;
4606 }
4607 if (!check_term_argument(term[1], check_rule_StateFrm<atermpp::aterm>))
4608 {
4609 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4610 return false;
4611 }
4612#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4613
4614#endif // MCRL2_NO_SOUNDNESS_CHECKS
4615 return true;
4616}
4617
4618// StateYaled()
4619template <typename Term>
4620bool check_term_StateYaled(const Term& t)
4621{
4623#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4624 // check the type of the term
4625 const atermpp::aterm& term(t);
4626 if (!term.type_is_appl())
4627 {
4628 return false;
4629 }
4631 {
4632 return false;
4633 }
4634
4635 // check the children
4636 if (term.size() != 0)
4637 {
4638 return false;
4639 }
4640
4641#endif // MCRL2_NO_SOUNDNESS_CHECKS
4642 return true;
4643}
4644
4645// StateYaledTimed(DataExpr)
4646template <typename Term>
4648{
4650#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4651 // check the type of the term
4652 const atermpp::aterm& term(t);
4653 if (!term.type_is_appl())
4654 {
4655 return false;
4656 }
4658 {
4659 return false;
4660 }
4661
4662 // check the children
4663 if (term.size() != 1)
4664 {
4665 return false;
4666 }
4667#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4668 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4669 {
4670 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
4671 return false;
4672 }
4673#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4674
4675#endif // MCRL2_NO_SOUNDNESS_CHECKS
4676 return true;
4677}
4678
4679// StateDelay()
4680template <typename Term>
4681bool check_term_StateDelay(const Term& t)
4682{
4684#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4685 // check the type of the term
4686 const atermpp::aterm& term(t);
4687 if (!term.type_is_appl())
4688 {
4689 return false;
4690 }
4692 {
4693 return false;
4694 }
4695
4696 // check the children
4697 if (term.size() != 0)
4698 {
4699 return false;
4700 }
4701
4702#endif // MCRL2_NO_SOUNDNESS_CHECKS
4703 return true;
4704}
4705
4706// StateDelayTimed(DataExpr)
4707template <typename Term>
4709{
4711#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4712 // check the type of the term
4713 const atermpp::aterm& term(t);
4714 if (!term.type_is_appl())
4715 {
4716 return false;
4717 }
4719 {
4720 return false;
4721 }
4722
4723 // check the children
4724 if (term.size() != 1)
4725 {
4726 return false;
4727 }
4728#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4729 if (!check_term_argument(term[0], check_rule_DataExpr<atermpp::aterm>))
4730 {
4731 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
4732 return false;
4733 }
4734#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4735
4736#endif // MCRL2_NO_SOUNDNESS_CHECKS
4737 return true;
4738}
4739
4740// StateVar(String, DataExpr*)
4741template <typename Term>
4742bool check_term_StateVar(const Term& t)
4743{
4745#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4746 // check the type of the term
4747 const atermpp::aterm& term(t);
4748 if (!term.type_is_appl())
4749 {
4750 return false;
4751 }
4753 {
4754 return false;
4755 }
4756
4757 // check the children
4758 if (term.size() != 2)
4759 {
4760 return false;
4761 }
4762#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4763 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4764 {
4765 mCRL2log(log::debug) << "check_rule_String" << std::endl;
4766 return false;
4767 }
4768 if (!check_list_argument(term[1], check_rule_DataExpr<atermpp::aterm>, 0))
4769 {
4770 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
4771 return false;
4772 }
4773#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4774
4775#endif // MCRL2_NO_SOUNDNESS_CHECKS
4776 return true;
4777}
4778
4779// StateNu(String, DataVarIdInit*, StateFrm)
4780template <typename Term>
4781bool check_term_StateNu(const Term& t)
4782{
4784#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4785 // check the type of the term
4786 const atermpp::aterm& term(t);
4787 if (!term.type_is_appl())
4788 {
4789 return false;
4790 }
4792 {
4793 return false;
4794 }
4795
4796 // check the children
4797 if (term.size() != 3)
4798 {
4799 return false;
4800 }
4801#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4802 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4803 {
4804 mCRL2log(log::debug) << "check_rule_String" << std::endl;
4805 return false;
4806 }
4807 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
4808 {
4809 mCRL2log(log::debug) << "check_rule_DataVarIdInit" << std::endl;
4810 return false;
4811 }
4812 if (!check_term_argument(term[2], check_rule_StateFrm<atermpp::aterm>))
4813 {
4814 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4815 return false;
4816 }
4817#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4818
4819#endif // MCRL2_NO_SOUNDNESS_CHECKS
4820 return true;
4821}
4822
4823// StateMu(String, DataVarIdInit*, StateFrm)
4824template <typename Term>
4825bool check_term_StateMu(const Term& t)
4826{
4828#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4829 // check the type of the term
4830 const atermpp::aterm& term(t);
4831 if (!term.type_is_appl())
4832 {
4833 return false;
4834 }
4836 {
4837 return false;
4838 }
4839
4840 // check the children
4841 if (term.size() != 3)
4842 {
4843 return false;
4844 }
4845#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4846 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
4847 {
4848 mCRL2log(log::debug) << "check_rule_String" << std::endl;
4849 return false;
4850 }
4851 if (!check_list_argument(term[1], check_rule_DataVarIdInit<atermpp::aterm>, 0))
4852 {
4853 mCRL2log(log::debug) << "check_rule_DataVarIdInit" << std::endl;
4854 return false;
4855 }
4856 if (!check_term_argument(term[2], check_rule_StateFrm<atermpp::aterm>))
4857 {
4858 mCRL2log(log::debug) << "check_rule_StateFrm" << std::endl;
4859 return false;
4860 }
4861#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4862
4863#endif // MCRL2_NO_SOUNDNESS_CHECKS
4864 return true;
4865}
4866
4867// RegNil()
4868template <typename Term>
4869bool check_term_RegNil(const Term& t)
4870{
4872#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4873 // check the type of the term
4874 const atermpp::aterm& term(t);
4875 if (!term.type_is_appl())
4876 {
4877 return false;
4878 }
4880 {
4881 return false;
4882 }
4883
4884 // check the children
4885 if (term.size() != 0)
4886 {
4887 return false;
4888 }
4889
4890#endif // MCRL2_NO_SOUNDNESS_CHECKS
4891 return true;
4892}
4893
4894// RegSeq(RegFrm, RegFrm)
4895template <typename Term>
4896bool check_term_RegSeq(const Term& t)
4897{
4899#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4900 // check the type of the term
4901 const atermpp::aterm& term(t);
4902 if (!term.type_is_appl())
4903 {
4904 return false;
4905 }
4907 {
4908 return false;
4909 }
4910
4911 // check the children
4912 if (term.size() != 2)
4913 {
4914 return false;
4915 }
4916#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4917 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4918 {
4919 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
4920 return false;
4921 }
4922 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4923 {
4924 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
4925 return false;
4926 }
4927#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4928
4929#endif // MCRL2_NO_SOUNDNESS_CHECKS
4930 return true;
4931}
4932
4933// RegAlt(RegFrm, RegFrm)
4934template <typename Term>
4935bool check_term_RegAlt(const Term& t)
4936{
4938#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4939 // check the type of the term
4940 const atermpp::aterm& term(t);
4941 if (!term.type_is_appl())
4942 {
4943 return false;
4944 }
4946 {
4947 return false;
4948 }
4949
4950 // check the children
4951 if (term.size() != 2)
4952 {
4953 return false;
4954 }
4955#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4956 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4957 {
4958 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
4959 return false;
4960 }
4961 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
4962 {
4963 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
4964 return false;
4965 }
4966#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4967
4968#endif // MCRL2_NO_SOUNDNESS_CHECKS
4969 return true;
4970}
4971
4972// RegTrans(RegFrm)
4973template <typename Term>
4974bool check_term_RegTrans(const Term& t)
4975{
4977#ifndef MCRL2_NO_SOUNDNESS_CHECKS
4978 // check the type of the term
4979 const atermpp::aterm& term(t);
4980 if (!term.type_is_appl())
4981 {
4982 return false;
4983 }
4985 {
4986 return false;
4987 }
4988
4989 // check the children
4990 if (term.size() != 1)
4991 {
4992 return false;
4993 }
4994#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
4995 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
4996 {
4997 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
4998 return false;
4999 }
5000#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5001
5002#endif // MCRL2_NO_SOUNDNESS_CHECKS
5003 return true;
5004}
5005
5006// RegTransOrNil(RegFrm)
5007template <typename Term>
5008bool check_term_RegTransOrNil(const Term& t)
5009{
5011#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5012 // check the type of the term
5013 const atermpp::aterm& term(t);
5014 if (!term.type_is_appl())
5015 {
5016 return false;
5017 }
5019 {
5020 return false;
5021 }
5022
5023 // check the children
5024 if (term.size() != 1)
5025 {
5026 return false;
5027 }
5028#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5029 if (!check_term_argument(term[0], check_rule_RegFrm<atermpp::aterm>))
5030 {
5031 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
5032 return false;
5033 }
5034#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5035
5036#endif // MCRL2_NO_SOUNDNESS_CHECKS
5037 return true;
5038}
5039
5040// UntypedRegFrm(String, RegFrm, RegFrm)
5041template <typename Term>
5042bool check_term_UntypedRegFrm(const Term& t)
5043{
5045#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5046 // check the type of the term
5047 const atermpp::aterm& term(t);
5048 if (!term.type_is_appl())
5049 {
5050 return false;
5051 }
5053 {
5054 return false;
5055 }
5056
5057 // check the children
5058 if (term.size() != 3)
5059 {
5060 return false;
5061 }
5062#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5063 if (!check_term_argument(term[0], check_rule_String<atermpp::aterm>))
5064 {
5065 mCRL2log(log::debug) << "check_rule_String" << std::endl;
5066 return false;
5067 }
5068 if (!check_term_argument(term[1], check_rule_RegFrm<atermpp::aterm>))
5069 {
5070 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
5071 return false;
5072 }
5073 if (!check_term_argument(term[2], check_rule_RegFrm<atermpp::aterm>))
5074 {
5075 mCRL2log(log::debug) << "check_rule_RegFrm" << std::endl;
5076 return false;
5077 }
5078#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5079
5080#endif // MCRL2_NO_SOUNDNESS_CHECKS
5081 return true;
5082}
5083
5084// ActTrue()
5085template <typename Term>
5086bool check_term_ActTrue(const Term& t)
5087{
5089#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5090 // check the type of the term
5091 const atermpp::aterm& term(t);
5092 if (!term.type_is_appl())
5093 {
5094 return false;
5095 }
5097 {
5098 return false;
5099 }
5100
5101 // check the children
5102 if (term.size() != 0)
5103 {
5104 return false;
5105 }
5106
5107#endif // MCRL2_NO_SOUNDNESS_CHECKS
5108 return true;
5109}
5110
5111// ActFalse()
5112template <typename Term>
5113bool check_term_ActFalse(const Term& t)
5114{
5116#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5117 // check the type of the term
5118 const atermpp::aterm& term(t);
5119 if (!term.type_is_appl())
5120 {
5121 return false;
5122 }
5124 {
5125 return false;
5126 }
5127
5128 // check the children
5129 if (term.size() != 0)
5130 {
5131 return false;
5132 }
5133
5134#endif // MCRL2_NO_SOUNDNESS_CHECKS
5135 return true;
5136}
5137
5138// ActNot(ActFrm)
5139template <typename Term>
5140bool check_term_ActNot(const Term& t)
5141{
5143#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5144 // check the type of the term
5145 const atermpp::aterm& term(t);
5146 if (!term.type_is_appl())
5147 {
5148 return false;
5149 }
5151 {
5152 return false;
5153 }
5154
5155 // check the children
5156 if (term.size() != 1)
5157 {
5158 return false;
5159 }
5160#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5161 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5162 {
5163 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5164 return false;
5165 }
5166#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5167
5168#endif // MCRL2_NO_SOUNDNESS_CHECKS
5169 return true;
5170}
5171
5172// ActAnd(ActFrm, ActFrm)
5173template <typename Term>
5174bool check_term_ActAnd(const Term& t)
5175{
5177#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5178 // check the type of the term
5179 const atermpp::aterm& term(t);
5180 if (!term.type_is_appl())
5181 {
5182 return false;
5183 }
5185 {
5186 return false;
5187 }
5188
5189 // check the children
5190 if (term.size() != 2)
5191 {
5192 return false;
5193 }
5194#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5195 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5196 {
5197 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5198 return false;
5199 }
5200 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5201 {
5202 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5203 return false;
5204 }
5205#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5206
5207#endif // MCRL2_NO_SOUNDNESS_CHECKS
5208 return true;
5209}
5210
5211// ActOr(ActFrm, ActFrm)
5212template <typename Term>
5213bool check_term_ActOr(const Term& t)
5214{
5216#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5217 // check the type of the term
5218 const atermpp::aterm& term(t);
5219 if (!term.type_is_appl())
5220 {
5221 return false;
5222 }
5224 {
5225 return false;
5226 }
5227
5228 // check the children
5229 if (term.size() != 2)
5230 {
5231 return false;
5232 }
5233#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5234 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5235 {
5236 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5237 return false;
5238 }
5239 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5240 {
5241 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5242 return false;
5243 }
5244#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5245
5246#endif // MCRL2_NO_SOUNDNESS_CHECKS
5247 return true;
5248}
5249
5250// ActImp(ActFrm, ActFrm)
5251template <typename Term>
5252bool check_term_ActImp(const Term& t)
5253{
5255#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5256 // check the type of the term
5257 const atermpp::aterm& term(t);
5258 if (!term.type_is_appl())
5259 {
5260 return false;
5261 }
5263 {
5264 return false;
5265 }
5266
5267 // check the children
5268 if (term.size() != 2)
5269 {
5270 return false;
5271 }
5272#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5273 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5274 {
5275 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5276 return false;
5277 }
5278 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5279 {
5280 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5281 return false;
5282 }
5283#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5284
5285#endif // MCRL2_NO_SOUNDNESS_CHECKS
5286 return true;
5287}
5288
5289// ActForall(DataVarId+, ActFrm)
5290template <typename Term>
5291bool check_term_ActForall(const Term& t)
5292{
5294#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5295 // check the type of the term
5296 const atermpp::aterm& term(t);
5297 if (!term.type_is_appl())
5298 {
5299 return false;
5300 }
5302 {
5303 return false;
5304 }
5305
5306 // check the children
5307 if (term.size() != 2)
5308 {
5309 return false;
5310 }
5311#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5312 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5313 {
5314 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
5315 return false;
5316 }
5317 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5318 {
5319 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5320 return false;
5321 }
5322#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5323
5324#endif // MCRL2_NO_SOUNDNESS_CHECKS
5325 return true;
5326}
5327
5328// ActExists(DataVarId+, ActFrm)
5329template <typename Term>
5330bool check_term_ActExists(const Term& t)
5331{
5333#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5334 // check the type of the term
5335 const atermpp::aterm& term(t);
5336 if (!term.type_is_appl())
5337 {
5338 return false;
5339 }
5341 {
5342 return false;
5343 }
5344
5345 // check the children
5346 if (term.size() != 2)
5347 {
5348 return false;
5349 }
5350#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5351 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 1))
5352 {
5353 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
5354 return false;
5355 }
5356 if (!check_term_argument(term[1], check_rule_ActFrm<atermpp::aterm>))
5357 {
5358 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5359 return false;
5360 }
5361#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5362
5363#endif // MCRL2_NO_SOUNDNESS_CHECKS
5364 return true;
5365}
5366
5367// ActAt(ActFrm, DataExpr)
5368template <typename Term>
5369bool check_term_ActAt(const Term& t)
5370{
5372#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5373 // check the type of the term
5374 const atermpp::aterm& term(t);
5375 if (!term.type_is_appl())
5376 {
5377 return false;
5378 }
5380 {
5381 return false;
5382 }
5383
5384 // check the children
5385 if (term.size() != 2)
5386 {
5387 return false;
5388 }
5389#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5390 if (!check_term_argument(term[0], check_rule_ActFrm<atermpp::aterm>))
5391 {
5392 mCRL2log(log::debug) << "check_rule_ActFrm" << std::endl;
5393 return false;
5394 }
5395 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
5396 {
5397 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
5398 return false;
5399 }
5400#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5401
5402#endif // MCRL2_NO_SOUNDNESS_CHECKS
5403 return true;
5404}
5405
5406// ActMultAct(Action*)
5407template <typename Term>
5408bool check_term_ActMultAct(const Term& t)
5409{
5411#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5412 // check the type of the term
5413 const atermpp::aterm& term(t);
5414 if (!term.type_is_appl())
5415 {
5416 return false;
5417 }
5419 {
5420 return false;
5421 }
5422
5423 // check the children
5424 if (term.size() != 1)
5425 {
5426 return false;
5427 }
5428#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5429 if (!check_list_argument(term[0], check_rule_Action<atermpp::aterm>, 0))
5430 {
5431 mCRL2log(log::debug) << "check_rule_Action" << std::endl;
5432 return false;
5433 }
5434#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5435
5436#endif // MCRL2_NO_SOUNDNESS_CHECKS
5437 return true;
5438}
5439
5440// ActionRenameRules(ActionRenameRule*)
5441template <typename Term>
5443{
5445#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5446 // check the type of the term
5447 const atermpp::aterm& term(t);
5448 if (!term.type_is_appl())
5449 {
5450 return false;
5451 }
5453 {
5454 return false;
5455 }
5456
5457 // check the children
5458 if (term.size() != 1)
5459 {
5460 return false;
5461 }
5462#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5463 if (!check_list_argument(term[0], check_rule_ActionRenameRule<atermpp::aterm>, 0))
5464 {
5465 mCRL2log(log::debug) << "check_rule_ActionRenameRule" << std::endl;
5466 return false;
5467 }
5468#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5469
5470#endif // MCRL2_NO_SOUNDNESS_CHECKS
5471 return true;
5472}
5473
5474// ActionRenameRule(DataVarId*, DataExpr, ParamIdOrAction, ActionRenameRuleRHS)
5475template <typename Term>
5477{
5479#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5480 // check the type of the term
5481 const atermpp::aterm& term(t);
5482 if (!term.type_is_appl())
5483 {
5484 return false;
5485 }
5487 {
5488 return false;
5489 }
5490
5491 // check the children
5492 if (term.size() != 4)
5493 {
5494 return false;
5495 }
5496#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5497 if (!check_list_argument(term[0], check_rule_DataVarId<atermpp::aterm>, 0))
5498 {
5499 mCRL2log(log::debug) << "check_rule_DataVarId" << std::endl;
5500 return false;
5501 }
5502 if (!check_term_argument(term[1], check_rule_DataExpr<atermpp::aterm>))
5503 {
5504 mCRL2log(log::debug) << "check_rule_DataExpr" << std::endl;
5505 return false;
5506 }
5507 if (!check_term_argument(term[2], check_rule_ParamIdOrAction<atermpp::aterm>))
5508 {
5509 mCRL2log(log::debug) << "check_rule_ParamIdOrAction" << std::endl;
5510 return false;
5511 }
5512 if (!check_term_argument(term[3], check_rule_ActionRenameRuleRHS<atermpp::aterm>))
5513 {
5514 mCRL2log(log::debug) << "check_rule_ActionRenameRuleRHS" << std::endl;
5515 return false;
5516 }
5517#endif // MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS
5518
5519#endif // MCRL2_NO_SOUNDNESS_CHECKS
5520 return true;
5521}
5522
5523// ActionRenameSpec(DataSpec, ActSpec, ActionRenameRules)
5524template <typename Term>
5526{
5528#ifndef MCRL2_NO_SOUNDNESS_CHECKS
5529 // check the type of the term
5530 const atermpp::aterm& term(t);
5531 if (!term.type_is_appl())
5532 {
5533 return false;
5534 }
5536 {
5537 return false;
5538 }
5539
5540 // check the children
5541 if (term.size() != 3)
5542 {
5543 return false;
5544 }
5545#ifndef MCRL2_NO_RECURSIVE_SOUNDNESS_CHECKS