Skip to content

gds_software.statemachine.checks

State machine verification checks (SM-001..SM-006).

SM-001: Exactly one initial state exists.

Source code in packages/gds-software/gds_software/statemachine/checks.py 
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
def check_sm001_initial_state(model: StateMachineModel) -> list[Finding]:
    """SM-001: Exactly one initial state exists."""
    initial = [s for s in model.states if s.is_initial]
    passed = len(initial) == 1
    return [
        Finding(
            check_id="SM-001",
            severity=Severity.ERROR,
            message=(
                f"State machine has {len(initial)} initial state(s), expected 1"
                if not passed
                else "State machine has exactly one initial state"
            ),
            source_elements=[s.name for s in initial] or ["<none>"],
            passed=passed,
        )
    ]

SM-002: All states are reachable from the initial state.

Source code in packages/gds-software/gds_software/statemachine/checks.py 
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
def check_sm002_reachability(model: StateMachineModel) -> list[Finding]:
    """SM-002: All states are reachable from the initial state."""
    if not any(s.is_initial for s in model.states):
        return []

    initial = model.initial_state
    # BFS from initial
    reachable: set[str] = set()
    queue = [initial.name]
    while queue:
        current = queue.pop(0)
        if current in reachable:
            continue
        reachable.add(current)
        for t in model.transitions:
            if t.source == current and t.target not in reachable:
                queue.append(t.target)

    findings: list[Finding] = []
    for state in model.states:
        is_reachable = state.name in reachable
        findings.append(
            Finding(
                check_id="SM-002",
                severity=Severity.WARNING,
                message=(
                    f"State {state.name!r} is not reachable from initial state"
                    if not is_reachable
                    else f"State {state.name!r} is reachable"
                ),
                source_elements=[state.name],
                passed=is_reachable,
            )
        )
    return findings

SM-003: No two transitions from the same state on the same event (without guards).

Source code in packages/gds-software/gds_software/statemachine/checks.py 
 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
104
105
106
107
108
109
110
111
112
def check_sm003_determinism(model: StateMachineModel) -> list[Finding]:
    """SM-003: No two transitions from the same state on the same event (without guards)."""
    findings: list[Finding] = []
    # Group transitions by (source, event)
    groups: dict[tuple[str, str], list[str]] = {}
    for t in model.transitions:
        key = (t.source, t.event)
        groups.setdefault(key, []).append(t.name)

    for (source, event), trans_names in groups.items():
        # Check if any of these transitions lack guards
        transitions = [t for t in model.transitions if t.name in trans_names]
        unguarded = [t for t in transitions if t.guard is None]

        if len(unguarded) > 1:
            findings.append(
                Finding(
                    check_id="SM-003",
                    severity=Severity.ERROR,
                    message=(
                        f"Non-deterministic: {len(unguarded)} unguarded transitions "
                        f"from {source!r} on event {event!r}: "
                        f"{[t.name for t in unguarded]}"
                    ),
                    source_elements=[t.name for t in unguarded],
                    passed=False,
                )
            )

    if not findings:
        findings.append(
            Finding(
                check_id="SM-003",
                severity=Severity.ERROR,
                message="State machine is deterministic",
                source_elements=[],
                passed=True,
            )
        )
    return findings

SM-004: Transitions with guards from same state/event should be exhaustive.

Source code in packages/gds-software/gds_software/statemachine/checks.py 
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
def check_sm004_guard_completeness(model: StateMachineModel) -> list[Finding]:
    """SM-004: Transitions with guards from same state/event should be exhaustive."""
    findings: list[Finding] = []
    groups: dict[tuple[str, str], list[str]] = {}
    for t in model.transitions:
        key = (t.source, t.event)
        groups.setdefault(key, []).append(t.name)

    for (source, event), trans_names in groups.items():
        transitions = [t for t in model.transitions if t.name in trans_names]
        guarded = [t for t in transitions if t.guard is not None]
        unguarded = [t for t in transitions if t.guard is None]

        if guarded and not unguarded:
            # All guarded, no default — may not be exhaustive
            findings.append(
                Finding(
                    check_id="SM-004",
                    severity=Severity.WARNING,
                    message=(
                        f"All transitions from {source!r} on {event!r} are guarded "
                        f"with no default — may not be exhaustive"
                    ),
                    source_elements=[t.name for t in guarded],
                    passed=False,
                )
            )

    if not findings:
        findings.append(
            Finding(
                check_id="SM-004",
                severity=Severity.WARNING,
                message="Guard completeness is satisfied",
                source_elements=[],
                passed=True,
            )
        )
    return findings

SM-005: Region states must partition the state set (no overlaps, no gaps).

Source code in packages/gds-software/gds_software/statemachine/checks.py 
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
def check_sm005_region_partition(model: StateMachineModel) -> list[Finding]:
    """SM-005: Region states must partition the state set (no overlaps, no gaps)."""
    if not model.regions:
        return [
            Finding(
                check_id="SM-005",
                severity=Severity.WARNING,
                message="No regions defined — partition check skipped",
                source_elements=[],
                passed=True,
            )
        ]

    findings: list[Finding] = []
    all_region_states: list[str] = []
    for region in model.regions:
        all_region_states.extend(region.states)

    # Check for overlaps
    seen: set[str] = set()
    for s in all_region_states:
        if s in seen:
            findings.append(
                Finding(
                    check_id="SM-005",
                    severity=Severity.ERROR,
                    message=f"State {s!r} appears in multiple regions",
                    source_elements=[s],
                    passed=False,
                )
            )
        seen.add(s)

    # Check for gaps
    for state in model.states:
        if state.name not in seen:
            findings.append(
                Finding(
                    check_id="SM-005",
                    severity=Severity.WARNING,
                    message=f"State {state.name!r} is not assigned to any region",
                    source_elements=[state.name],
                    passed=False,
                )
            )

    if not findings:
        findings.append(
            Finding(
                check_id="SM-005",
                severity=Severity.WARNING,
                message="Region partition is valid",
                source_elements=[],
                passed=True,
            )
        )
    return findings

SM-006: Transition source/target are declared states, events are declared.

Source code in packages/gds-software/gds_software/statemachine/checks.py 
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
def check_sm006_transition_validity(model: StateMachineModel) -> list[Finding]:
    """SM-006: Transition source/target are declared states, events are declared."""
    findings: list[Finding] = []
    for t in model.transitions:
        src_valid = t.source in model.state_names
        findings.append(
            Finding(
                check_id="SM-006",
                severity=Severity.ERROR,
                message=(
                    f"Transition {t.name!r} source {t.source!r} "
                    f"{'is' if src_valid else 'is NOT'} a declared state"
                ),
                source_elements=[t.name, t.source],
                passed=src_valid,
            )
        )
        tgt_valid = t.target in model.state_names
        findings.append(
            Finding(
                check_id="SM-006",
                severity=Severity.ERROR,
                message=(
                    f"Transition {t.name!r} target {t.target!r} "
                    f"{'is' if tgt_valid else 'is NOT'} a declared state"
                ),
                source_elements=[t.name, t.target],
                passed=tgt_valid,
            )
        )
        evt_valid = t.event in model.event_names
        findings.append(
            Finding(
                check_id="SM-006",
                severity=Severity.ERROR,
                message=(
                    f"Transition {t.name!r} event {t.event!r} "
                    f"{'is' if evt_valid else 'is NOT'} a declared event"
                ),
                source_elements=[t.name, t.event],
                passed=evt_valid,
            )
        )
    return findings