-- specification AG (!Idle) is false
-- as demonstrated by the following execution sequence
state 1.1:
unchanged_except_dispatcher_a1 = 0
unchanged_except_dispatcher_adt__wrapper = 0
unchanged_except_dispatcher_a2 = 0
unchanged_except_dispatcher = 0
unchanged_except_artist__manager_client_... = 0
unchanged_except_artist__manager_a1 = 0
unchanged_except_artist__manager_a2 = 0
unchanged_except_artist__manager = 0
unchanged_except_adt__wrapper_client__in... = 0
unchanged_except_a2_artist__manager = 0
unchanged_except_a2_dispatcher = 0
unchanged_except_a1_artist__manager = 0
unchanged_except_a1_dispatcher = 0
a1_enabled = 0
a2_enabled = 0
adt__wrapper_enabled = 0
artist__manager_enabled = 1
client__init_enabled = 1
dispatcher_enabled = 0
Idle = 0
dispatcher = s1
client__init = s1
artist__manager = s1
adt__wrapper = s1
a2 = s1
a1 = s1

state 1.2:
a1_enabled = 1
client__init_enabled = 0
client__init = s2
artist__manager = s2

state 1.3:
a2_enabled = 1
dispatcher_enabled = 1
artist__manager = s3
a1 = s2

state 1.4:
dispatcher = s33
a1 = s3

state 1.5:
artist__manager_enabled = 0
artist__manager = s4
a2 = s2

state 1.6:
artist__manager_enabled = 1
dispatcher = s21
a1 = s4

state 1.7:
a2_enabled = 0
dispatcher_enabled = 0
dispatcher = s15
a2 = s3

state 1.8:
a1_enabled = 0
a2_enabled = 1
artist__manager = s5
a1 = s5

state 1.9:
a2_enabled = 0
client__init_enabled = 1
artist__manager = s6
a2 = s4

state 1.10:
a1_enabled = 1
adt__wrapper_enabled = 1
client__init = s3
artist__manager = s8

state 1.11:
client__init_enabled = 0
dispatcher_enabled = 1
client__init = s4
adt__wrapper = s3

state 1.12:
adt__wrapper_enabled = 0
dispatcher = s93
adt__wrapper = s4

state 1.13:
a1_enabled = 0
artist__manager_enabled = 0
dispatcher_enabled = 0
Idle = 1
artist__manager = s9
a1 = s6


resources used:
user time: 0.19 s, system time: 0.03 s
BDD nodes allocated: 15524
Bytes allocated: 1507328
BDD nodes representing transition relation: 3448 + 13