Joeri Exelmans aed0f352e4 Fix some things 2 年 前
..
README.txt b62fc3a6e7 Add readme for semantics example 4 年 前
run.py aed0f352e4 Fix some things 2 年 前
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 年 前
statechart_semantics.xml b148794d66 Fixed semantics example (was broken due to runtime changes). 3 年 前

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.