/* Promela specification for problem ./sedl/dispa */


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_register__e2__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__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
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_18
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_15
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto state_13
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto state_11
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto state_9
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto state_7
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto state_5
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto state_3
  :: 0 -> goto endstate_2
  fi;
endstate_2:
  0;
state_3:
  if
  :: dispatch__e1_register__e1__chan!synch__art2 -> goto state_4
  fi;
state_4:
  if
  :: dispatcher_register__event_end__chan?synch -> goto endstate_1
  fi;
state_5:
  if
  :: dispatch__e2_register__e2__chan!synch__art1 -> goto state_4
  fi;
state_7:
  if
  :: dispatch__e1_register__e1__chan!synch__art1 -> goto state_4
  fi;
state_9:
  if
  :: dispatch__e1_unregister__e1__chan!synch__art2 -> goto state_10
  fi;
state_10:
  if
  :: dispatcher_unregister__event_end__chan?synch -> goto endstate_1
  fi;
state_11:
  if
  :: dispatch__e2_unregister__e2__chan!synch__art1 -> goto state_10
  fi;
state_13:
  if
  :: dispatch__e1_unregister__e1__chan!synch__art1 -> goto state_10
  fi;
state_15:
  if
  :: dispatch__e2_notify__e2__chan!synch -> goto state_16
  fi;
state_16:
  if
  :: dispatch__e2_notify__e2_end__chan!synch -> goto state_17
  fi;
state_17:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_1
  fi;
state_18:
  if
  :: dispatch__e1_notify__e1__chan!synch -> goto state_19
  fi;
state_19:
  if
  :: dispatch__e1_notify__e1_end__chan!synch -> goto state_17
  fi
}

proctype dispatch__e2()
{
endstate_1:
  if
  :: dispatch__e2_notify__e2__chan?synch -> goto state_50
  :: dispatch__e2_unregister__e2__chan?synch__art1 -> goto endstate_1
  :: dispatch__e2_register__e2__chan?synch__art1 -> goto endstate_19
  :: 0 -> goto endstate_2
  fi;
endstate_2:
  0;
endstate_19:
  if
  :: dispatch__e2_notify__e2__chan?synch -> goto state_25
  :: dispatch__e2_unregister__e2__chan?synch__art1 -> goto endstate_1
  :: dispatch__e2_register__e2__chan?synch__art1 -> goto endstate_19
  :: 0 -> goto endstate_2
  fi;
state_25:
  if
  :: a1_notify__client__event__chan!synch__e2 -> goto state_26
  fi;
state_26:
  if
  :: dispatch__e2_notify__e2_end__chan?synch -> goto endstate_19
  fi;
state_50:
  if
  :: dispatch__e2_notify__e2_end__chan?synch -> goto endstate_1
  fi
}

proctype dispatch__e1()
{
endstate_1:
  if
  :: dispatch__e1_notify__e1__chan?synch -> goto state_50
  :: dispatch__e1_unregister__e1__chan?synch__art1 -> goto endstate_1
  :: dispatch__e1_unregister__e1__chan?synch__art2 -> goto endstate_1
  :: dispatch__e1_register__e1__chan?synch__art1 -> goto endstate_19
  :: dispatch__e1_register__e1__chan?synch__art2 -> goto endstate_3
  :: 0 -> goto endstate_2
  fi;
endstate_2:
  0;
endstate_3:
  if
  :: dispatch__e1_notify__e1__chan?synch -> goto state_48
  :: dispatch__e1_unregister__e1__chan?synch__art1 -> goto endstate_3
  :: dispatch__e1_unregister__e1__chan?synch__art2 -> goto endstate_1
  :: dispatch__e1_register__e1__chan?synch__art1 -> goto endstate_7
  :: dispatch__e1_register__e1__chan?synch__art2 -> goto endstate_3
  :: 0 -> goto endstate_2
  fi;
endstate_7:
  if
  :: dispatch__e1_notify__e1__chan?synch -> goto state_42
  :: dispatch__e1_unregister__e1__chan?synch__art1 -> goto endstate_3
  :: dispatch__e1_unregister__e1__chan?synch__art2 -> goto endstate_19
  :: dispatch__e1_register__e1__chan?synch__art1 -> goto endstate_7
  :: dispatch__e1_register__e1__chan?synch__art2 -> goto endstate_7
  :: 0 -> goto endstate_2
  fi;
endstate_13:
  if
  :: dispatch__e1_notify__e1__chan?synch -> goto state_34
  :: dispatch__e1_unregister__e1__chan?synch__art1 -> goto endstate_3
  :: dispatch__e1_unregister__e1__chan?synch__art2 -> goto endstate_19
  :: dispatch__e1_register__e1__chan?synch__art1 -> goto endstate_13
  :: dispatch__e1_register__e1__chan?synch__art2 -> goto endstate_13
  :: 0 -> goto endstate_2
  fi;
endstate_19:
  if
  :: dispatch__e1_notify__e1__chan?synch -> goto state_25
  :: dispatch__e1_unregister__e1__chan?synch__art1 -> goto endstate_1
  :: dispatch__e1_unregister__e1__chan?synch__art2 -> goto endstate_19
  :: dispatch__e1_register__e1__chan?synch__art1 -> goto endstate_19
  :: dispatch__e1_register__e1__chan?synch__art2 -> goto endstate_13
  :: 0 -> goto endstate_2
  fi;
state_25:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_26
  fi;
state_26:
  if
  :: dispatch__e1_notify__e1_end__chan?synch -> goto endstate_19
  fi;
state_34:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_35
  fi;
state_35:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_36
  fi;
state_36:
  if
  :: dispatch__e1_notify__e1_end__chan?synch -> goto endstate_13
  fi;
state_42:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_43
  fi;
state_43:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_44
  fi;
state_44:
  if
  :: dispatch__e1_notify__e1_end__chan?synch -> goto endstate_7
  fi;
state_48:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_49
  fi;
state_49:
  if
  :: dispatch__e1_notify__e1_end__chan?synch -> goto endstate_3
  fi;
state_50:
  if
  :: dispatch__e1_notify__e1_end__chan?synch -> goto endstate_1
  fi
}

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

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

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

proctype a2()
{
state_1:
  if
  :: a2_start__artist__chan?synch -> goto state_2
  fi;
state_2:
  if
  :: dispatcher_register__event__chan!synch__art2_e1 -> goto state_3
  fi;
state_3:
  if
  :: dispatcher_register__event_end__chan!synch -> goto state_4
  fi;
state_4:
  if
  :: artist__manager_a2__registered__chan!synch -> goto state_5
  fi;
state_5:
  if
  :: a2_notify__client__event__chan?synch__e1 -> goto state_5
  :: a2_terminate__artist__chan?synch -> goto state_6
  fi;
state_6:
  if
  :: dispatcher_unregister__event__chan!synch__art2_e1 -> goto state_12
  fi;
state_12:
  if
  :: dispatcher_unregister__event_end__chan!synch -> goto state_13
  fi;
state_13:
  if
  :: a2_terminate__artist_end__chan?synch -> goto endstate_14
  fi;
endstate_14:
  0
}

proctype a1()
{
state_1:
  if
  :: a1_start__artist__chan?synch -> goto state_2
  fi;
state_2:
  if
  :: dispatcher_register__event__chan!synch__art1_e1 -> goto state_3
  fi;
state_3:
  if
  :: dispatcher_register__event_end__chan!synch -> goto state_4
  fi;
state_4:
  if
  :: dispatcher_register__event__chan!synch__art1_e2 -> goto state_5
  fi;
state_5:
  if
  :: dispatcher_register__event_end__chan!synch -> goto state_6
  fi;
state_6:
  if
  :: artist__manager_a1__registered__chan!synch -> goto state_7
  fi;
state_7:
  if
  :: a1_notify__client__event__chan?synch__e1 -> goto state_7
  :: a1_notify__client__event__chan?synch__e2 -> goto state_7
  :: a1_terminate__artist__chan?synch -> goto state_8
  fi;
state_8:
  if
  :: dispatcher_unregister__event__chan!synch__art1_e1 -> goto state_16
  fi;
state_16:
  if
  :: dispatcher_unregister__event_end__chan!synch -> goto state_17
  fi;
state_17:
  if
  :: dispatcher_unregister__event__chan!synch__art1_e2 -> goto state_18
  fi;
state_18:
  if
  :: dispatcher_unregister__event_end__chan!synch -> goto state_19
  fi;
state_19:
  if
  :: a1_terminate__artist_end__chan?synch -> 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()
  }
}

/* beforeregistera1e1 = 
(BEFORE "call(a1;dispatcher.register_event;art1;e1)")
*/
#define beforeregistera1e1 (a1[8]@state_2)

/* isregistereda1e1 = 
(IN-TASK DISPATCH_E1
 (OR (AND (>= E1_SZ 1) (= "art1" (INDEX E1_LST 1)))
     (AND (>= E1_SZ 2) (= "art1" (INDEX E1_LST 2)))))
*/
#define isregistereda1e1 (dispatch__e1[3]@state_44 \
    || dispatch__e1[3]@state_43 \
    || dispatch__e1[3]@state_42 \
    || dispatch__e1[3]@state_36 \
    || dispatch__e1[3]@state_35 \
    || dispatch__e1[3]@state_34 \
    || dispatch__e1[3]@state_26 \
    || dispatch__e1[3]@state_25 \
    || dispatch__e1[3]@endstate_19 \
    || dispatch__e1[3]@endstate_13 \
    || dispatch__e1[3]@endstate_7)


#include "p01a1e1.never"