Is there a way to verif/ validate a state machine ?

[hwerbi]

Python State Machine version: 0.8.0
Python version: 3.7
Operating System: windows 10

Description

I created a state machine for a system and now I would like to validate the state machine. Something like to proof that the state machine does not contain a block senario, if it's ambiguous? Is it deterministic?
Or even to test some LTL formule on it ?

Is there a way to do this ? with python, model cheker ?

[fgmacedo]

@hwerbi , we've implemented a few checks built-in:

• Are there states defined?
• Are there transitions defined?
• Is there one and only one initial state?
• Is the statemachine graph a single component? (Is there any disconected sub-graph? Unheachable states?)

Other tests can be performed the same way, please see

python-statemachine/statemachine/statemachine.py

Lines 348 to 371 in cee0e83

	def check(self):
	if not self.states:
	raise InvalidDefinition(_('There are no states.'))
	if not self.transitions:
	raise InvalidDefinition(_('There are no transitions.'))
	initials = [s for s in self.states if s.initial]
	if len(initials) != 1:
	raise InvalidDefinition(_('There should be one and only one initial state. '
	'Your currently have these: {!r}'.format(initials)))
	self.initial_state = initials[0]
	disconnected_states = self._disconnected_states(self.initial_state)
	if (disconnected_states):
	raise InvalidDefinition(_('There are unreachable states. '
	'The statemachine graph should have a single component. '
	'Disconnected states: [{}]'.format(disconnected_states)))
	if self.current_state_value is None:
	if self.start_value:
	self.current_state_value = self.start_value
	else:
	self.current_state_value = self.initial_state.value

Let me know if I can help with something, feel free to reopen the issue.