/* Promela specification for problem ./sedl/dispb */
bit notifyclienteventa2e1 = 0;
bit notifyclienteventa1e1 = 0;


mtype = { synch,
   synch__art2_e1,
   synch__art1_e2,
   synch__art1_e1,
   synch__e2,
   synch__e1 }

chan dispatcher_register__event__chan = [0] of { mtype };
chan dispatcher_unregister__event__chan = [0] of { mtype };
chan dispatcher_notify__artists__chan = [0] of { mtype };
chan dispatcher_notify__artists_end__chan = [0] of { mtype };
chan artist__manager_start__manager__chan = [0] of { mtype };
chan artist__manager_a1__registered__chan = [0] of { mtype };
chan artist__manager_a2__registered__chan = [0] of { mtype };
chan artist__manager_start__manager_end__chan = [0] of { mtype };
chan adt__wrapper_start__wrapper__chan = [0] of { mtype };
chan a2_start__artist__chan = [0] of { mtype };
chan a2_terminate__artist__chan = [0] of { mtype };
chan a2_notify__client__event__chan = [0] of { mtype };
chan a2_terminate__artist_end__chan = [0] of { mtype };
chan a1_start__artist__chan = [0] of { mtype };
chan a1_terminate__artist__chan = [0] of { mtype };
chan a1_notify__client__event__chan = [0] of { mtype };
chan a1_terminate__artist_end__chan = [0] of { mtype };

proctype dispatcher()
{
endstate_1:
  if
  :: atomic { dispatcher_register__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_33
  :: atomic { dispatcher_register__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_27
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_40
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_39
  :: atomic { dispatcher_register__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_2:
  0;
endstate_3:
  if
  :: atomic { dispatcher_unregister__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  :: atomic { dispatcher_register__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_57
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_76
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_75
  :: atomic { dispatcher_register__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_5
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_5:
  if
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  :: atomic { dispatcher_unregister__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_27
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_90
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_88
  :: atomic { dispatcher_register__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_59
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_13:
  if
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_100
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_99
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  :: atomic { dispatcher_unregister__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_33
  :: atomic { dispatcher_register__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_15:
  if
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_95
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_93
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_5
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_13
  :: atomic { dispatcher_unregister__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_21
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_21:
  if
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_48
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_46
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_27
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_33
  :: atomic { dispatcher_register__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_27:
  if
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_31
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_29
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  :: atomic { dispatcher_register__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_21
  :: atomic { dispatcher_register__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_5
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
state_29:
  if
  :: atomic { a1_notify__client__event__chan!synch__e2 } -> goto state_30
  fi;
state_30:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_27
  fi;
state_31:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_30
  fi;
endstate_33:
  if
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_36
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_35
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  :: atomic { dispatcher_register__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_21
  :: atomic { dispatcher_register__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_13
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
state_35:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_33
  fi;
state_36:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_37
  fi;
state_37:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_35
  fi;
state_39:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  fi;
state_40:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_39
  fi;
state_46:
  if
  :: atomic { a1_notify__client__event__chan!synch__e2 } -> goto state_47
  fi;
state_47:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_21
  fi;
state_48:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_49
  fi;
state_49:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_47
  fi;
endstate_57:
  if
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_80
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_79
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  :: atomic { dispatcher_unregister__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_33
  :: atomic { dispatcher_register__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_59
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_59:
  if
  :: atomic { dispatcher_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_63
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_61
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_5
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_57
  :: atomic { dispatcher_unregister__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_21
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
state_61:
  if
  :: atomic { a1_notify__client__event__chan!synch__e2 } -> goto state_62
  fi;
state_62:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_59
  fi;
state_63:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_64
  fi;
state_64:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_65
  fi;
state_65:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_62
  fi;
state_75:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  fi;
state_76:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_77
  fi;
state_77:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_75
  fi;
state_79:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_57
  fi;
state_80:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_81
  fi;
state_81:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_82
  fi;
state_82:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_79
  fi;
state_88:
  if
  :: atomic { a1_notify__client__event__chan!synch__e2 } -> goto state_89
  fi;
state_89:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_5
  fi;
state_90:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_91
  fi;
state_91:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_89
  fi;
state_93:
  if
  :: atomic { a1_notify__client__event__chan!synch__e2 } -> goto state_94
  fi;
state_94:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  fi;
state_95:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_96
  fi;
state_96:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_97
  fi;
state_97:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_94
  fi;
state_99:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_13
  fi;
state_100:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_101
  fi;
state_101:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_102
  fi;
state_102:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_99
  fi
}

proctype client__init()
{
state_1:
  if
  :: atomic { artist__manager_start__manager__chan!synch } -> goto state_2
  fi;
state_2:
  if
  :: atomic { artist__manager_start__manager_end__chan!synch } -> goto state_3
  fi;
state_3:
  if
  :: atomic { adt__wrapper_start__wrapper__chan!synch } -> goto endstate_4
  fi;
endstate_4:
  0
}

proctype artist__manager()
{
state_1:
  if
  :: atomic { artist__manager_start__manager__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_2
  fi;
state_2:
  if
  :: atomic { a1_start__artist__chan!synch } -> goto state_3
  fi;
state_3:
  if
  :: atomic { a2_start__artist__chan!synch } -> goto state_4
  fi;
state_4:
  if
  :: atomic { artist__manager_a1__registered__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_5
  fi;
state_5:
  if
  :: atomic { artist__manager_a2__registered__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_6
  fi;
state_6:
  if
  :: atomic { artist__manager_start__manager_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_8
  :: atomic { artist__manager_start__manager_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_7
  fi;
state_7:
  goto state_7_loop;
state_7_loop:
  goto state_7;
;
state_8:
  if
  :: atomic { a1_terminate__artist__chan!synch } -> goto state_9
  fi;
state_9:
  if
  :: atomic { a1_terminate__artist_end__chan!synch } -> goto state_10
  fi;
state_10:
  if
  :: atomic { a2_terminate__artist__chan!synch } -> goto state_11
  fi;
state_11:
  if
  :: atomic { a2_terminate__artist_end__chan!synch } -> goto endstate_12
  fi;
endstate_12:
  0
}

proctype adt__wrapper()
{
state_1:
  if
  :: atomic { adt__wrapper_start__wrapper__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_3
  :: atomic { adt__wrapper_start__wrapper__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_2
  fi;
state_2:
  if
  :: atomic { dispatcher_notify__artists__chan!synch__e1 } -> goto state_4
  fi;
state_3:
  if
  :: atomic { dispatcher_notify__artists__chan!synch__e2 } -> goto state_4
  fi;
state_4:
  if
  :: atomic { dispatcher_notify__artists_end__chan!synch } -> goto state_3
  :: atomic { dispatcher_notify__artists_end__chan!synch } -> goto state_2
  fi
}

proctype a2()
{
state_1:
  if
  :: atomic { a2_start__artist__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_2
  fi;
state_2:
  if
  :: atomic { dispatcher_register__event__chan!synch__art2_e1 } -> goto state_3
  fi;
state_3:
  if
  :: atomic { artist__manager_a2__registered__chan!synch } -> goto state_4
  fi;
state_4:
  if
  :: atomic { a2_notify__client__event__chan?synch__e1;
              notifyclienteventa2e1 = 1;
              notifyclienteventa1e1 = 0 } -> goto state_4
  :: atomic { a2_terminate__artist__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_5
  fi;
state_5:
  if
  :: atomic { dispatcher_unregister__event__chan!synch__art2_e1 } -> goto state_10
  fi;
state_10:
  if
  :: atomic { a2_terminate__artist_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_11
  fi;
endstate_11:
  0
}

proctype a1()
{
state_1:
  if
  :: atomic { a1_start__artist__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_2
  fi;
state_2:
  if
  :: atomic { dispatcher_register__event__chan!synch__art1_e1 } -> goto state_3
  fi;
state_3:
  if
  :: atomic { dispatcher_register__event__chan!synch__art1_e2 } -> goto state_4
  fi;
state_4:
  if
  :: atomic { artist__manager_a1__registered__chan!synch } -> goto state_5
  fi;
state_5:
  if
  :: atomic { a1_notify__client__event__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 1 } -> goto state_5
  :: atomic { a1_notify__client__event__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_5
  :: atomic { a1_terminate__artist__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_6
  fi;
state_6:
  if
  :: atomic { dispatcher_unregister__event__chan!synch__art1_e1 } -> goto state_12
  fi;
state_12:
  if
  :: atomic { dispatcher_unregister__event__chan!synch__art1_e2 } -> goto state_13
  fi;
state_13:
  if
  :: atomic { a1_terminate__artist_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_14
  fi;
endstate_14:
  0
}

init {
  atomic { run dispatcher();
    run client__init();
    run artist__manager();
    run adt__wrapper();
    run a2();
    run a1()
  }
}

/* e1szEQ0 = 
(IN-TASK DISPATCHER (= E1_SZ 0))
*/
#define e1szEQ0 (dispatcher[1]@state_40 \
    || dispatcher[1]@state_39 \
    || dispatcher[1]@state_31 \
    || dispatcher[1]@state_30 \
    || dispatcher[1]@state_29 \
    || dispatcher[1]@endstate_27 \
    || dispatcher[1]@endstate_2 \
    || dispatcher[1]@endstate_1)


#include "p05a.never"