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


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
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_1
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_1
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_1
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_29
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_33
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_38
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_38
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_3
  :: 0 -> goto endstate_2
  fi;
endstate_2:
  0;
endstate_3:
  if
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_3
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_3
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_1
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_66
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_79
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_78
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_5
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_3
  :: 0 -> goto endstate_2
  fi;
endstate_5:
  if
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_5
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_3
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_33
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_98
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_96
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_9
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_5
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_5
  :: 0 -> goto endstate_2
  fi;
endstate_9:
  if
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_120
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_118
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_5
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_66
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_23
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_9
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_9
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_9
  :: 0 -> goto endstate_2
  fi;
endstate_15:
  if
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_106
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_104
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_5
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_19
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_23
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_15
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_15
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_15
  :: 0 -> goto endstate_2
  fi;
endstate_19:
  if
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_85
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_84
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_3
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_19
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_29
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_19
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_15
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_19
  :: 0 -> goto endstate_2
  fi;
endstate_23:
  if
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_33
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_29
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_53
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_51
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_23
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_23
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_23
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_15
  :: 0 -> goto endstate_2
  fi;
endstate_29:
  if
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_41
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_40
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_1
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_29
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_29
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_29
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_23
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_19
  :: 0 -> goto endstate_2
  fi;
endstate_33:
  if
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_36
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_35
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_33
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_1
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_33
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_23
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_33
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_5
  :: 0 -> goto endstate_2
  fi;
state_35:
  if
  :: a1_notify__client__event__chan!synch__e2 -> goto state_36
  fi;
state_36:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_33
  fi;
state_38:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_1
  fi;
state_40:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_29
  fi;
state_41:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_40
  fi;
state_51:
  if
  :: a1_notify__client__event__chan!synch__e2 -> goto state_52
  fi;
state_52:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_23
  fi;
state_53:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_52
  fi;
endstate_66:
  if
  :: dispatcher_notify__artists__chan?synch__e1 -> goto state_69
  :: dispatcher_notify__artists__chan?synch__e2 -> goto state_68
  :: dispatcher_unregister__event__chan?synch__art1_e1 -> goto endstate_3
  :: dispatcher_unregister__event__chan?synch__art1_e2 -> goto endstate_66
  :: dispatcher_unregister__event__chan?synch__art2_e1 -> goto endstate_29
  :: dispatcher_register__event__chan?synch__art1_e1 -> goto endstate_66
  :: dispatcher_register__event__chan?synch__art1_e2 -> goto endstate_9
  :: dispatcher_register__event__chan?synch__art2_e1 -> goto endstate_66
  :: 0 -> goto endstate_2
  fi;
state_68:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_66
  fi;
state_69:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_70
  fi;
state_70:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_68
  fi;
state_78:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_3
  fi;
state_79:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_78
  fi;
state_84:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_19
  fi;
state_85:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_86
  fi;
state_86:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_84
  fi;
state_96:
  if
  :: a1_notify__client__event__chan!synch__e2 -> goto state_97
  fi;
state_97:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_5
  fi;
state_98:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_97
  fi;
state_104:
  if
  :: a1_notify__client__event__chan!synch__e2 -> goto state_105
  fi;
state_105:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_15
  fi;
state_106:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_107
  fi;
state_107:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_105
  fi;
state_118:
  if
  :: a1_notify__client__event__chan!synch__e2 -> goto state_119
  fi;
state_119:
  if
  :: dispatcher_notify__artists_end__chan?synch -> goto endstate_9
  fi;
state_120:
  if
  :: a2_notify__client__event__chan!synch__e1 -> goto state_121
  fi;
state_121:
  if
  :: a1_notify__client__event__chan!synch__e1 -> goto state_119
  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
  :: artist__manager_a2__registered__chan!synch -> goto state_4
  fi;
state_4:
  if
  :: a2_notify__client__event__chan?synch__e1 -> goto state_4
  :: a2_terminate__artist__chan?synch -> goto state_5
  fi;
state_5:
  if
  :: dispatcher_unregister__event__chan!synch__art2_e1 -> goto state_10
  fi;
state_10:
  if
  :: a2_terminate__artist_end__chan?synch -> goto endstate_11
  fi;
endstate_11:
  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__chan!synch__art1_e2 -> goto state_4
  fi;
state_4:
  if
  :: artist__manager_a1__registered__chan!synch -> goto state_5
  fi;
state_5:
  if
  :: a1_notify__client__event__chan?synch__e1 -> goto state_5
  :: a1_notify__client__event__chan?synch__e2 -> goto state_5
  :: a1_terminate__artist__chan?synch -> goto state_6
  fi;
state_6:
  if
  :: dispatcher_unregister__event__chan!synch__art1_e1 -> goto state_12
  fi;
state_12:
  if
  :: dispatcher_unregister__event__chan!synch__art1_e2 -> goto state_13
  fi;
state_13:
  if
  :: a1_terminate__artist_end__chan?synch -> goto endstate_14
  fi;
endstate_14:
  0
}

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

/* beforeunregistera1e1 = 
(BEFORE "call(a1;dispatcher.unregister_event;art1;e1)")
*/
#define beforeunregistera1e1 (a1[6]@state_6)

/* isregistereda1e1 = 
(IN-TASK DISPATCHER
 (OR (AND (>= E1_SZ 1) (= "art1" (INDEX E1_LST 1)))
     (AND (>= E1_SZ 2) (= "art1" (INDEX E1_LST 2)))))
*/
#define isregistereda1e1 (dispatcher[1]@state_121 \
    || dispatcher[1]@state_120 \
    || dispatcher[1]@state_119 \
    || dispatcher[1]@state_118 \
    || dispatcher[1]@state_107 \
    || dispatcher[1]@state_106 \
    || dispatcher[1]@state_105 \
    || dispatcher[1]@state_104 \
    || dispatcher[1]@state_86 \
    || dispatcher[1]@state_85 \
    || dispatcher[1]@state_84 \
    || dispatcher[1]@state_70 \
    || dispatcher[1]@state_69 \
    || dispatcher[1]@state_68 \
    || dispatcher[1]@endstate_66 \
    || dispatcher[1]@state_53 \
    || dispatcher[1]@state_52 \
    || dispatcher[1]@state_51 \
    || dispatcher[1]@state_41 \
    || dispatcher[1]@state_40 \
    || dispatcher[1]@endstate_29 \
    || dispatcher[1]@endstate_23 \
    || dispatcher[1]@endstate_19 \
    || dispatcher[1]@endstate_15 \
    || dispatcher[1]@endstate_9)


#include "p01b.never"