-- specification AG (!Idle) is false
-- as demonstrated by the following execution sequence
state 1.1:
unchanged_except_dispatcher_adt__wrapper = 0
unchanged_except_dispatcher_a1 = 0
unchanged_except_dispatcher_a2 = 0
unchanged_except_dispatcher = 0
unchanged_except_dispatch__e2_dispatcher = 0
unchanged_except_dispatch__e1_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_dispatch__e1 = 0
unchanged_except_a1_artist__manager = 0
unchanged_except_a1_dispatch__e1 = 0
unchanged_except_a1_dispatch__e2 = 0
a1_enabled = 0
a2_enabled = 0
adt__wrapper_enabled = 0
artist__manager_enabled = 1
client__init_enabled = 1
dispatch__e1_enabled = 0
dispatch__e2_enabled = 0
dispatcher_enabled = 0
Idle = 0
dispatcher = s1
dispatch__e2 = s1
dispatch__e1 = 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:
a1_enabled = 0
dispatch__e1_enabled = 1
dispatcher = s7
a1 = s3

state 1.5:
a1_enabled = 1
dispatch__e1_enabled = 0
dispatcher = s4
dispatch__e1 = s15

state 1.6:
dispatcher = s1
a1 = s4

state 1.7:
a1_enabled = 0
dispatch__e2_enabled = 1
dispatcher = s5
a1 = s5

state 1.8:
a1_enabled = 1
dispatch__e2_enabled = 0
dispatcher = s4
dispatch__e2 = s15

state 1.9:
a2_enabled = 0
artist__manager_enabled = 0
artist__manager = s4
a2 = s2

state 1.10:
a2_enabled = 1
artist__manager_enabled = 1
dispatcher = s1
a1 = s6

state 1.11:
a2_enabled = 0
dispatch__e1_enabled = 1
dispatcher = s3
a2 = s3

state 1.12:
a2_enabled = 1
dispatch__e1_enabled = 0
dispatcher = s4
dispatch__e1 = s9

state 1.13:
a1_enabled = 0
artist__manager_enabled = 0
artist__manager = s5
a1 = s7

state 1.14:
artist__manager_enabled = 1
dispatcher_enabled = 0
dispatcher = s1
a2 = s4

state 1.15:
a2_enabled = 0
client__init_enabled = 1
artist__manager = s6
a2 = s5

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

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

state 1.18:
adt__wrapper_enabled = 0
dispatch__e2_enabled = 1
dispatcher = s15
adt__wrapper = s4

state 1.19:
dispatcher_enabled = 0
dispatcher = s16
dispatch__e2 = s17

state 1.20:
a1_enabled = 0
artist__manager_enabled = 0
dispatch__e2_enabled = 0
Idle = 1
artist__manager = s9
a1 = s8


resources used:
user time: 0.33 s, system time: 0.03 s
BDD nodes allocated: 26490
Bytes allocated: 1638400
BDD nodes representing transition relation: 5641 + 19