--- CISC/CMPE 422, CISC 835
--- ASSIGNMENT 4
--- Author: Juergen Dingel

MODULE Generator(N, out)
-- input: 'N' is number of non-'nil' outputs to generate
-- output: 'out' is one of {destA, destB, destC, destD, nil}
-- DON'T MODIFY!

VAR
  c: 0..N;          -- number of non-'nil' coutries picked
  cA: 0..N;         -- number of times 'destA' has been picked
  cB: 0..N;
  cC: 0..N;
  cD: 0..N;
  done: boolean;    -- set when loop counter i reaches N
  pc: {             -- program counter
          checking,
          computing,
          outputting
      };
ASSIGN
  init(c):=0;
  init(cA):=0;
  init(cB):=0;
  init(cC):=0;
  init(cD):=0;
  init(done):=FALSE;
  init(pc):=checking;
  next(out):=
    case
      pc=checking : nil; -- no output is produced while we check
      pc=computing : {destA, destB, destC, destD};  -- pick a destination non-deterministically
      pc=outputting: nil;  -- reset output
    esac;
  next(c):=
    case
      pc=computing & next(out)!=nil & c<N : c+1;  -- increment count of all pieces generated
      TRUE : c;
    esac;
  next(cA):=
    case
      pc=computing & next(out)=destA & cA<N : cA+1;  -- increment count of pieces destined for destA generated
      TRUE : cA;
    esac;
  next(cB):=
    case
      pc=computing & next(out)=destB & cB<N : cB+1;  -- increment count of pieces destined for destB generated
      TRUE : cB;
    esac;
  next(cC):=
    case
      pc=computing & next(out)=destC & cC<N : cC+1;  -- increment count of pieces destined for destC generated
      TRUE : cC;
    esac;
  next(cD):=
    case
      pc=computing & next(out)=destD & cD<N : cD+1;  -- increment count of pieces destined for destD generated
      TRUE : cD;
    esac;
  next(done):=
    case
      pc=outputting & c=N: TRUE; -- done
      TRUE: done;
    esac;
  next(pc):=
    case
      pc=checking & c<N : computing; -- not done yet; start another iteration
      pc=computing : outputting; -- output what has been produced
      pc=outputting : checking; -- start again
      TRUE : pc;
    esac;
-- END MODULE Generator(N, out)

MODULE Switch(inp, level, leftOut, rightOut)
VAR
  pc: {one, two, three};
  inpCopy: {destA, destB, destC, destD, nil};
  dir: {left, right};
ASSIGN
  init(pc):= one;
  init(inpCopy):= nil;
  init(dir):= {left, right};  -- arbitrary initialization
  next(pc) :=
	case
		pc=one & inp=nil : one;
		pc=one & inp!=nil : two;
		pc=two : three;
		pc=three : one;
		TRUE : one;
	esac;
  next(inpCopy):=
	case
		pc=one : inp;
		pc=three: nil;
		TRUE : inpCopy;
    esac;
  next(dir):=
	case
		pc=two & level=0 & (inpCopy=destA | inpCopy=destB): left;
		pc=two & level=0 & (inpCopy=destC | inpCopy=destD): right;
		pc=two & level=1 & (inpCopy=destA | inpCopy=destC): left;
		pc=two & level=1 & (inpCopy=destB | inpCopy=destD): right;
		TRUE: right;
	esac;
  next(leftOut):=
	case
		pc=three & dir=left : inpCopy;
		TRUE: nil;
	esac;
  next(rightOut):=
	case
		pc=three & dir=right : inpCopy;
		TRUE: nil;
	esac;
-- END MODULE Switch(inp, level, leftOut, rightOut)

MODULE Bin(dest, inp, N)
-- input: 'dest' is destination this bin is for, 'inp' is where the input is delivered, and
--        'N' is the number of pieces to generate
-- DON'T MODIFY!
VAR
  cnt: 0..N;
  err: 0..N;
ASSIGN
  init(cnt):= 0;
  init(err):= 0;
  next(cnt):= case
		  inp=dest & cnt<N: cnt+1; -- increment count of correctly delivered pieces
		  TRUE: cnt;
	      esac;
  next(err):= case
		inp!=nil & inp!=dest & err<N : err+1; -- increment count of incorrectly delivered pieces
		TRUE: err;
	      esac;
-- END MODULE Bin(dest, inp, N)

MODULE main
-- Creates sorter, sets 'N', and initializes shared variables
-- No need to modify, except for changing the value of 'N'
DEFINE
  N := 8;
VAR
  g_to_s1 : {destA, destB, destC, destD, nil};
  s1_to_s2 : {destA, destB, destC, destD, nil};
  s1_to_s3 : {destA, destB, destC, destD, nil};
  s2_to_bA : {destA, destB, destC, destD, nil};
  s2_to_bB : {destA, destB, destC, destD, nil};
  s3_to_bC : {destA, destB, destC, destD, nil};
  s3_to_bD : {destA, destB, destC, destD, nil};
  g: Generator(N, g_to_s1);
  s1: Switch(g_to_s1, 0, s1_to_s2, s1_to_s3);
  s2: Switch(s1_to_s2, 1, s2_to_bA, s2_to_bB);
  s3: Switch(s1_to_s3, 1, s3_to_bC, s3_to_bD);
  bA: Bin(destA, s2_to_bA, N);
  bB: Bin(destB, s2_to_bB, N);
  bC: Bin(destC, s3_to_bC, N);
  bD: Bin(destD, s3_to_bD, N);
ASSIGN
  init(g_to_s1):= nil;
  init(s1_to_s2) := nil;
  init(s1_to_s3) := nil;
  init(s2_to_bA) := nil;
  init(s2_to_bB) := nil;
  init(s3_to_bC) := nil;
  init(s3_to_bD) := nil;
-- END MODULE main

---- QUESTION 1 -------------------------------------------------------------------------------
--- Item a)
-- "After two execution steps from the initial state, the generator will always be outputting"
SPEC AX AX g.pc=outputting
-- "The generator only produces non-nil output"
SPEC AG (g.pc=outputting -> g_to_s1!=nil)
-- "The total number of pieces of luggage generated is always equal to the sum of the numbers generated for each of the four destinations"
SPEC AG g.c=(g.cA+g.cB+g.cC+g.cD)
-- "The total number of pieces generated is never greater than the number of pieces requested"
SPEC AG g.c<=N
-- "The generator will always eventually stop"
SPEC AF g.done

--- Item b)
-- "Whenever generator has generated the requested number of pieces of luggage, then it is done"
-- This is incorrect because g.c could equal N but g could be in a state other than done
-- By changing the g.done imlpies g.c=N we know if the generator is done, the requested must equal the generated
SPEC AG (g.done -> g.c=N) -- false, uncomment to generate counter example
-- your corrected version here

-- "The generator is capable of eventually outputting a piece destined for each of the four destinations"
-- This is incorerct because what if g is done, then it can not produce a piece.
-- We have to ensure the generator isn't finished and also it can only go to a single destination
-- so we change the ors to ands.
SPEC AG (!g.done ->(EF g_to_s1=destA) | (EF g_to_s1=destB) | (EF g_to_s1=destC) | (EF g_to_s1=destD)) -- false
-- your corrected version here

-- "Whenever the generator is producing output, then along any sequence of three execution steps it will again produce output"
SPEC AG (g.pc = outputting & AX !g.done -> AX AX AX g.pc = outputting ) -- false
-- your corrected version here

---- QUESTION 2 -------------------------------------------------------------------------------
-- Your CTL formulas for Item c) here

-- "Whenever a specific non-nil input arrives at switch s1, then s1 will always output that input to switch s2 two steps later, and s2 will always output that input to bin bA four steps later"
--SPEC AG (s1.inp != nil -> ((AX AX s2.inp = s1.inp) & (AX AX AX AX AX AX bA.inp = s1.inp)))

-- "Switch s1 will never output a non-nil value to switch s3"
--SPEC AG (s1_to_s3 = nil)

-- "It is possible for value destA to arrive at bin bA"
SPEC EF (bA.inp = destA)

-- "The number of pieces of luggage that have arrived at bins bB, bC, and bD is always zero"
--SPEC AG (bB.cnt = 0 & bC.cnt = 0 & bD.cnt = 0)

-- "Along all executions, the number of pieces of luggage that have arrived at bin bA correctly and incorrectly, will eventually be equal to the requested number of pieces"
--SPEC AF (bA.N = (bA.cnt + bA.err))

-- "It is possible for no pieces for destination destA to be generated, i.e., there exists an execution along which eventually the number of pieces that have errorneously arrived at bin bA is equal to the requested number of pieces"
--SPEC EF (bA.err = bA.N)

---- QUESTION 3 -------------------------------------------------------------------------------
-- Your answers to the questions in Items b) to d) here
--"Along all paths, whenever the generator outputs a specific destination, then that output always arrives at the correct bin six steps later"
SPEC AF (g.out != nil -> ((g.out = destA & AX AX AX AX AX AX bA.inp = g.out) | (g.out = destB & AX AX AX AX AX AX bB.inp = g.out) | (g.out = destC & AX AX AX AX AX AX bC.inp = g.out) | (g.out = destD & AX AX AX AX AX AX bD.inp = g.out)))

--"Along all paths, eventually, done is set and the sum of the number of pieces correctly placed into all bins is equal to the number of requested pieces"
SPEC AG ((EF g.done) & (EF (bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.N))

--"The error counters of all bins are always equal to zero"
SPEC AG (bA.err = 0 & bB.err = 0 & bC.err = 0 & bD.err = 0)

SPEC EF (s1.inpCopy != nil & s2.inpCopy != nil & s3.inpCopy != nil)
SPEC EF (s1.inpCopy != nil & s2.inpCopy != nil)
SPEC EF (s2.inpCopy != nil & s3.inpCopy != nil)
SPEC EF (s1.inpCopy != nil & s3.inpCopy != nil)


SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 1)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 2)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 3)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 4)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 5)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 6)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 7)
SPEC EF((bA.cnt + bB.cnt + bC.cnt + bD.cnt) = g.c - 8)