-- This is the FDR script described in sections 5-5

-- CHECK_A requires elfReady and threeElves reports to be made.

-- CHECK_A checks that santa never reports threeElves until
-- at least three elves have reported elfReady.

-- FDR RESULTS:
--
-- SYSTEM deadlock free [F]                3,579 sec     156,210,432 ticks
-- SYSTEM deadlock free [FD]	          18,396 sec     156,210,432 ticks
-- SYSTEM livelock free                   21,063 sec     156,210,432 ticks
--	
-- CHECK_A_SYSTEM deadlock free [F]        3,571 sec     156,210,432 ticks
-- CHECK_A_SYSTEM deadlock free [FD]      35,578 sec     156,210,432 ticks
-- CHECK_A_SYSTEM livelock free           17,819 sec     156,210,432 ticks 

N_REINDEER = 9      -- number of reindeer
G_REINDEER = 9      -- number of reindeer needed to meet Santa

N_ELVES = 10        -- number of elves
G_ELVES = 3         -- number of elves needed to meet Santa

HOLIDAY_TIME = 42
WORKING_TIME = 42
CONSULTATION_TIME = 42
DELIVERY_TIME = 42

nametype R_set = {0..(N_REINDEER - 1)}         -- reindeer ids
nametype E_set = {0..(N_ELVES - 1)}            -- elf ids

datatype ReportTag =
    holiday | deerReady | deliver | deerDone |               -- reindeer reports
    working | elfReady | elfWaiting | consult | elfDone |    -- elf reports
    allReindeer | harness | mushMush | woah | unharness |    -- santa reindeer reports
    threeElves | greet | consulting | done | goodbye         -- santa elf reports

channel report : ReportTag.E_set               -- report.id (E_set includes R_set)

channel reindeer_2_santa : R_set               -- reindeer id
channel reindeer_2_santa_ack

channel elves_2_santa : E_set                  -- elf id
channel elves_2_santa_ack

channel just_elves_ping, just_elves_a, just_elves_b    -- extended partial barrier
channel santa_elves_a, santa_elves_b                   -- partial barrier
  
channel just_reindeer, santa_reindeer          -- barriers

REINDEER (id) =
    -- report ! holiday.id -> 
    RANDOM_TIMEOUT (HOLIDAY_TIME) ;
    -- report ! deerReady.id -> 
    just_reindeer ->
    reindeer_2_santa ! id -> santa_reindeer ->
    -- report ! deliver.id -> 
    santa_reindeer ->
    -- report ! deerDone.id -> 
    reindeer_2_santa ! id ->
    reindeer_2_santa_ack -> REINDEER (id)

RANDOM_TIMEOUT (TIME) = SKIP

P_BAR (n) =
    let
        PBAR = 
            (; x:<1..n> @ (santa_elves_a -> SKIP)) ;
            (; x:<1..n> @ (santa_elves_b -> SKIP)) ; PBAR
    within
        PBAR

XP_BAR (n) =
    let
        XPB =
            (; x:<1..n> @ (just_elves_a -> SKIP)) ;
            just_elves_ping -> 
            (; x:<1..n> @ (just_elves_b -> SKIP)) ; XPB
    within
        XPB

ELF (id) =
    -- report ! working.id -> 
    RANDOM_TIMEOUT (WORKING_TIME) ;
    report ! elfReady.id ->              -- this message is being checked
    just_elves_a -> just_elves_b ->
    elves_2_santa ! id ->
    santa_elves_a -> santa_elves_b ->
    -- report ! consult.id -> 
    santa_elves_a -> santa_elves_b ->
    -- report ! elfDone.id -> 
    elves_2_santa ! id ->
    elves_2_santa_ack -> ELF (id)

SANTA =
    (reindeer_2_santa ? id ->
      report ! allReindeer.0 -> 
      -- report ! harness.id ->
      (; x:<0..(G_REINDEER - 2)> @
        (reindeer_2_santa ? id ->
	     -- report ! harness.id -> 
	     SKIP)) ;
      -- report ! mushMush.0 -> 
      santa_reindeer ->
      RANDOM_TIMEOUT (DELIVERY_TIME) ; 
      -- report ! woah.0 -> 
      santa_reindeer ->
      (; x:<0..(G_REINDEER - 1)> @
        (reindeer_2_santa ? id -> 
	     -- report ! unharness.id ->
         reindeer_2_santa_ack -> SKIP)) ;
      SANTA
    )
    []
    (just_elves_ping ->
      report ! threeElves.0 ->         -- this message is also being checked
      (; x:<0..(G_ELVES - 1)> @
        (elves_2_santa ? id -> 
	     -- report ! greet.id -> 
	     SKIP)) ;
      -- report ! consulting.0 -> 
      santa_elves_a -> santa_elves_b ->
      RANDOM_TIMEOUT (CONSULTATION_TIME) ; 
      -- report ! done.0 -> 
      santa_elves_a -> santa_elves_b ->
      (; x:<0..(G_ELVES - 1)> @
        (elves_2_santa ? id -> 
	     -- report ! goodbye.id ->
         elves_2_santa_ack -> SKIP)) ;
      SANTA
    )



ALL_REINDEER =
    ([| {just_reindeer, santa_reindeer} |] id:R_set @ REINDEER (id))
    \ {just_reindeer}

ALL_ELVES = ||| id:E_set @ ELF (id)

XP_ELVES =
    ( ALL_ELVES [| {just_elves_a, just_elves_b} |] XP_BAR (G_ELVES) )
    \ {just_elves_a, just_elves_b}

SANTA_XP_ELVES =
    ( SANTA [| {| just_elves_ping, elves_2_santa, elves_2_santa_ack |} |] XP_ELVES )
    \ {| just_elves_ping, elves_2_santa, elves_2_santa_ack |}

SANTA_XP_P_ELVES =
    ( SANTA_XP_ELVES [| {santa_elves_a, santa_elves_b} |] P_BAR (G_ELVES + 1) )
    \ {santa_elves_a, santa_elves_b}

SYSTEM =
    ( SANTA_XP_P_ELVES [| {| santa_reindeer, reindeer_2_santa, reindeer_2_santa_ack |} |] ALL_REINDEER )
    \ {| santa_reindeer, reindeer_2_santa, reindeer_2_santa_ack |}

assert SYSTEM :[ deadlock free [F] ]
assert SYSTEM :[ deadlock free [FD] ]
assert SYSTEM :[ divergence free ]

CHECK_A (n) = 
    report ? x.y ->
      if x == elfReady then
        if n > N_ELVES then STOP else CHECK_A (n+1)
      else if x == threeElves then
        if n < G_ELVES then STOP else CHECK_A (n-G_ELVES)
      else
        CHECK_A (n)

CHECK_A_SYSTEM = SYSTEM [| {| report |} |] CHECK_A (0)

assert CHECK_A_SYSTEM :[ deadlock free [F] ]
assert CHECK_A_SYSTEM :[ deadlock free [FD] ]
assert CHECK_A_SYSTEM :[ divergence free ]