Separate core properties and their assertions

[MattWindsor91]

Currently, assertions over core properties are a distinct language from assertions over specifications. This is a holdover from the RoboChart Assertions language.

specification group Foo: module M
  // not used

assertion A: target of Foo is deterministic in the traces model

I think I would instead prefer to have something like:

specification group Foo: module M
  property Det: target is deterministic

assertion A: Foo::Det holds in the traces model // holds and does-not-hold allowed here

Advantages of doing this include:

• Assertion language is simplified and uniform (it now only knows about universal/existential properties and their negations);
• All properties of a target are under its group;
• Paves the way to eventually possibly making assertions able to target multiple properties at once (maybe an 'all properties of Foo hold in the traces model');
• Any future work in enriching the constant instantiation setup will be easier to apply to core properties.

Disadvantages include:

• More metamodel complexity;
• More verbose elucidation of core properties, unless we find a shorthand for asserting them.

From the metamodel perspective, we would end up with something like:

• Property
  • CoreProperty
  • Interaction
• Assertion (holds name, Property reference, negation, existential/universal)