Joeri Exelmans b3d7175114 Extend readme. Add some comments. 4 years ago
..
README.txt b62fc3a6e7 Add readme for semantics example 4 years ago
run.py b3d7175114 Extend readme. Add some comments. 4 years ago
statechart_semantics.svg 490196c118 Add script that checks if "semantic oracle" statechart correctly infers semantics under all circumstances. Small 'refactor' to how combo-step maximality option is represented in abstract syntax (now the same as big-step maximality). 4 years ago
statechart_semantics.xml e1826ed316 Made it possible to disable hierarchical priority. Added more priority tests, including tests that fail because of detected nondeterminism. 4 years ago

README.txt

This example contains a statechart that will, under a wide range of semantics, tell you the semantics being used to execute the model, by being in a certain configuration after the execution of 1 big-step.

The script 'run.py' checks if the statechart model correctly infers the semantics being used. The statechart model itself contains a semantic configuration of multiple variants, indicated by comma-separated lists of options for each semantic aspect. The SCCD runtime can generate all possible combinations for the options chosen, by taking the cross-product. This cross-product however, still contains some variants that cannot be detected correctly by the model, because they have invalid semantic configurations, or identically to other (simpler) variants. These "invalid variants" are filtered out by the script. The small set of rules for detecting "invalid variants" were constructed in an iterative way, and they partition the variants perfectly into valid/invalid.