/* 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,
   synch__art1,
   synch__art2 }

chan dispatcher_register__event__chan = [0] of { mtype };
chan dispatcher_register__event_end__chan = [0] of { mtype };
chan dispatcher_unregister__event__chan = [0] of { mtype };
chan dispatcher_unregister__event_end__chan = [0] of { mtype };
chan dispatcher_notify__artists__chan = [0] of { mtype };
chan dispatcher_notify__artists_end__chan = [0] of { mtype };
chan dispatch__e2_unregister__e2__chan = [0] of { mtype };
chan dispatch__e2_notify__e2__chan = [0] of { mtype };
chan dispatch__e2_notify__e2_end__chan = [0] of { mtype };
chan dispatch__e2_register__e2__chan = [0] of { mtype };
chan dispatch__e1_register__e1__chan = [0] of { mtype };
chan dispatch__e1_unregister__e1__chan = [0] of { mtype };
chan dispatch__e1_notify__e1__chan = [0] of { mtype };
chan dispatch__e1_notify__e1_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_notify__artists__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_18
  :: atomic { dispatcher_notify__artists__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_15
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_13
  :: atomic { dispatcher_unregister__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_11
  :: atomic { dispatcher_unregister__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_9
  :: atomic { dispatcher_register__event__chan?synch__art1_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_7
  :: atomic { dispatcher_register__event__chan?synch__art1_e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_5
  :: atomic { dispatcher_register__event__chan?synch__art2_e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_3
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_2:
  0;
state_3:
  if
  :: atomic { dispatch__e1_register__e1__chan!synch__art2 } -> goto state_4
  fi;
state_4:
  if
  :: atomic { dispatcher_register__event_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  fi;
state_5:
  if
  :: atomic { dispatch__e2_register__e2__chan!synch__art1 } -> goto state_4
  fi;
state_7:
  if
  :: atomic { dispatch__e1_register__e1__chan!synch__art1 } -> goto state_4
  fi;
state_9:
  if
  :: atomic { dispatch__e1_unregister__e1__chan!synch__art2 } -> goto state_10
  fi;
state_10:
  if
  :: atomic { dispatcher_unregister__event_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  fi;
state_11:
  if
  :: atomic { dispatch__e2_unregister__e2__chan!synch__art1 } -> goto state_10
  fi;
state_13:
  if
  :: atomic { dispatch__e1_unregister__e1__chan!synch__art1 } -> goto state_10
  fi;
state_15:
  if
  :: atomic { dispatch__e2_notify__e2__chan!synch } -> goto state_16
  fi;
state_16:
  if
  :: atomic { dispatch__e2_notify__e2_end__chan!synch } -> goto state_17
  fi;
state_17:
  if
  :: atomic { dispatcher_notify__artists_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  fi;
state_18:
  if
  :: atomic { skip;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_19
  fi;
state_19:
  if
  :: atomic { dispatch__e1_notify__e1__chan!synch } -> goto state_20
  fi;
state_20:
  if
  :: atomic { dispatch__e1_notify__e1_end__chan!synch } -> goto state_17
  fi
}

proctype dispatch__e2()
{
endstate_1:
  if
  :: atomic { dispatch__e2_notify__e2__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_32
  :: atomic { dispatch__e2_register__e2__chan?synch__art1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_2:
  0;
endstate_15:
  if
  :: atomic { dispatch__e2_notify__e2__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_17
  :: atomic { dispatch__e2_unregister__e2__chan?synch__art1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
state_17:
  if
  :: atomic { a1_notify__client__event__chan!synch__e2 } -> goto state_18
  fi;
state_18:
  if
  :: atomic { dispatch__e2_notify__e2_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  fi;
state_32:
  if
  :: atomic { dispatch__e2_notify__e2_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  fi
}

proctype dispatch__e1()
{
endstate_1:
  if
  :: atomic { dispatch__e1_notify__e1__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_32
  :: atomic { dispatch__e1_register__e1__chan?synch__art1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  :: atomic { dispatch__e1_register__e1__chan?synch__art2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_2:
  0;
endstate_3:
  if
  :: atomic { dispatch__e1_notify__e1__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_30
  :: atomic { dispatch__e1_unregister__e1__chan?synch__art2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  :: atomic { dispatch__e1_register__e1__chan?synch__art1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_5
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_5:
  if
  :: atomic { dispatch__e1_notify__e1__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_27
  :: atomic { dispatch__e1_unregister__e1__chan?synch__art1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  :: atomic { dispatch__e1_unregister__e1__chan?synch__art2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_9:
  if
  :: atomic { dispatch__e1_notify__e1__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_22
  :: atomic { dispatch__e1_unregister__e1__chan?synch__art1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  :: atomic { dispatch__e1_unregister__e1__chan?synch__art2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
endstate_15:
  if
  :: atomic { dispatch__e1_notify__e1__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_17
  :: atomic { dispatch__e1_unregister__e1__chan?synch__art1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  :: atomic { dispatch__e1_register__e1__chan?synch__art2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_9
  :: atomic { 0;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_2
  fi;
state_17:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_18
  fi;
state_18:
  if
  :: atomic { dispatch__e1_notify__e1_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_15
  fi;
state_22:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_23
  fi;
state_23:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_24
  fi;
state_24:
  if
  :: atomic { dispatch__e1_notify__e1_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_9
  fi;
state_27:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_28
  fi;
state_28:
  if
  :: atomic { a1_notify__client__event__chan!synch__e1 } -> goto state_29
  fi;
state_29:
  if
  :: atomic { dispatch__e1_notify__e1_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_5
  fi;
state_30:
  if
  :: atomic { a2_notify__client__event__chan!synch__e1 } -> goto state_31
  fi;
state_31:
  if
  :: atomic { dispatch__e1_notify__e1_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_3
  fi;
state_32:
  if
  :: atomic { dispatch__e1_notify__e1_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_1
  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 { dispatcher_register__event_end__chan!synch } -> goto state_4
  fi;
state_4:
  if
  :: atomic { artist__manager_a2__registered__chan!synch } -> goto state_5
  fi;
state_5:
  if
  :: atomic { a2_notify__client__event__chan?synch__e1;
              notifyclienteventa2e1 = 1;
              notifyclienteventa1e1 = 0 } -> goto state_5
  :: atomic { a2_terminate__artist__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_6
  fi;
state_6:
  if
  :: atomic { dispatcher_unregister__event__chan!synch__art2_e1 } -> goto state_12
  fi;
state_12:
  if
  :: atomic { dispatcher_unregister__event_end__chan!synch } -> goto state_13
  fi;
state_13:
  if
  :: atomic { a2_terminate__artist_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_14
  fi;
endstate_14:
  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_end__chan!synch } -> goto state_4
  fi;
state_4:
  if
  :: atomic { dispatcher_register__event__chan!synch__art1_e2 } -> goto state_5
  fi;
state_5:
  if
  :: atomic { dispatcher_register__event_end__chan!synch } -> goto state_6
  fi;
state_6:
  if
  :: atomic { artist__manager_a1__registered__chan!synch } -> goto state_7
  fi;
state_7:
  if
  :: atomic { a1_notify__client__event__chan?synch__e1;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 1 } -> goto state_7
  :: atomic { a1_notify__client__event__chan?synch__e2;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_7
  :: atomic { a1_terminate__artist__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto state_8
  fi;
state_8:
  if
  :: atomic { dispatcher_unregister__event__chan!synch__art1_e1 } -> goto state_16
  fi;
state_16:
  if
  :: atomic { dispatcher_unregister__event_end__chan!synch } -> goto state_17
  fi;
state_17:
  if
  :: atomic { dispatcher_unregister__event__chan!synch__art1_e2 } -> goto state_18
  fi;
state_18:
  if
  :: atomic { dispatcher_unregister__event_end__chan!synch } -> goto state_19
  fi;
state_19:
  if
  :: atomic { a1_terminate__artist_end__chan?synch;
              notifyclienteventa2e1 = 0;
              notifyclienteventa1e1 = 0 } -> goto endstate_20
  fi;
endstate_20:
  0
}

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

/* e1szEQ0 = 
(IN-TASK DISPATCH_E1 (= E1_SZ 0))
*/
#define e1szEQ0 (dispatch__e1[3]@state_32 \
    || dispatch__e1[3]@endstate_2 \
    || dispatch__e1[3]@endstate_1)


#include "p05a.never"