Daniel Plagge at 08:07, 6 January 2012

2012-01-06T08:07:06Z

← Older revision		Revision as of 08:07, 6 January 2012
Line 6:		Line 6:
	; <span style="color:#cd5c5c;">red</span> : The operation leads to a state where the invariant is violated.		; <span style="color:#cd5c5c;">red</span> : The operation leads to a state where the invariant is violated.
	; <span style="color:#cd6600;">orange</span> : The operation leads to a deadlock state, i.e. a state where no operation is enabled.		; <span style="color:#cd6600;">orange</span> : The operation leads to a deadlock state, i.e. a state where no operation is enabled.
	; <span style="color:#000000;">black</span> : Otherwise, the operation leads to a state that is different to the current state, has already been visited and is neither a invariant violating or deadlock state.		; <span style="color:#000000;">black</span> : Otherwise, the operation leads to a state that is different to the current state, has already been visited and is neither an invariant violating or deadlock state.

Daniel Plagge: Created page with 'The enabled operations are shown in different colours, depending on the state where the operation leads to. If more than one rule of the following list apply, the first colour is…'

2012-01-06T07:57:57Z

Created page with 'The enabled operations are shown in different colours, depending on the state where the operation leads to. If more than one rule of the following list apply, the first colour is…'

New page

The enabled operations are shown in different colours, depending on the state where the operation leads to.
If more than one rule of the following list apply, the first colour is taken:

; blue : The operation does not change the state (behaves like skip).
; green : The operation leads to a new, not yet explored state.
; red : The operation leads to a state where the invariant is violated.
; orange : The operation leads to a deadlock state, i.e. a state where no operation is enabled.
; black : Otherwise, the operation leads to a state that is different to the current state, has already been visited and is neither a invariant violating or deadlock state.

Colours of enabled operations - Revision history

Daniel Plagge at 08:07, 6 January 2012

Daniel Plagge: Created page with 'The enabled operations are shown in different colours, depending on the state where the operation leads to. If more than one rule of the following list apply, the first colour is…'