1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
/*
* SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
*
* SPDX-License-Identifier: EPL-2.0
*/
export default `% Metamodel
abstract class CompositeElement {
contains Region[] regions
}
class Region {
contains Vertex[] vertices opposite region
}
abstract class Vertex {
container Region region opposite vertices
contains Transition[] outgoingTransition opposite source
Transition[] incomingTransition opposite target
}
class Transition {
container Vertex source opposite outgoingTransition
Vertex[1] target opposite incomingTransition
}
abstract class Pseudostate extends Vertex.
abstract class RegularState extends Vertex.
class Entry extends Pseudostate.
class Exit extends Pseudostate.
class Choice extends Pseudostate.
class FinalState extends RegularState.
class State extends RegularState, CompositeElement.
class Statechart extends CompositeElement.
% Constraints
%% Entry
pred entryInRegion(Region r, Entry e) <->
vertices(r, e).
error noEntryInRegion(Region r) <->
!entryInRegion(r, _).
error multipleEntryInRegion(Region r) <->
entryInRegion(r, e1),
entryInRegion(r, e2),
e1 != e2.
error incomingToEntry(Transition t, Entry e) <->
target(t, e).
error noOutgoingTransitionFromEntry(Entry e) <->
!source(_, e).
error multipleTransitionFromEntry(Entry e, Transition t1, Transition t2) <->
outgoingTransition(e, t1),
outgoingTransition(e, t2),
t1 != t2.
%% Exit
error outgoingFromExit(Transition t, Exit e) <->
source(t, e).
%% Final
error outgoingFromFinal(Transition t, FinalState e) <->
source(t, e).
%% State vs Region
pred stateInRegion(Region r, State s) <->
vertices(r, s).
error noStateInRegion(Region r) <->
!stateInRegion(r, _).
%% Choice
error choiceHasNoOutgoing(Choice c) <->
!source(_, c).
error choiceHasNoIncoming(Choice c) <->
!target(_, c).
% Instance model
Statechart(sct).
% Scope
scope node = 20..30, Region = 2..*, Choice = 1..*, Statechart += 0.
`;
|
