For instance, Microsoft??™s DSL Tools take this approach, although
admittedly such model checking scripts are programmed in C# or using the GAT
framework, rather than the T4 template language used for other generators.
Another aspect where model checking reports differ from other generators is that
they often want to check the existence of a certain kind of item, or the number of those
items. TheDSMtool??™s modeling language facilities often support rules to check upper
bounds: for example, a Start state may have at most one transition leaving it. Checking
lower bounds is however harder, since such a rule could not be checked all the time:
adding a Start state to an empty model would be illegal, making it impossible to get
started on the model. Lower bound checks are thus often left to checking reports or
generators, which the user can run when desired.
Overenthusiastic or bossy metamodelers may be tempted to make such checks
compulsory, but that only invites the wrath of modelers when they need to save their
work and get out of the of?¬?ce quickly. Such solutions invariably cause more problems
than they solve: to pass the checks, the modeler will simply add fake elements to the
model. Sometimes those elements will be overlooked the next time, and since no
checking report will reveal them, they will remain until your customer ?¬?nds them for
you.
Pages:
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516