% Baxter model - abstracted to discrete system to model check
% Save this file in "neurons.sal"
% Model check property p0 using the command "sal-smc -v 3 neurons p0" 
% Use similar command for all other properties (listed at the end of this file).
neurons: CONTEXT =

BEGIN
  N: NATURAL = 4;
  LEVELS: TYPE = [0 .. N];
  SIGS: TYPE = { pos, neg, zero };
  NEURONS: TYPE = { B31, B35, B63, B34, B64, B4, B51, B52, B8, Z };
  PHASES: TYPE = { protraction, retraction, termination };

  GNEURONS(n: NEURONS): BOOLEAN = ( n /= B31 AND n /= B64 );

  % A generic model of a neurons; parameterized by its name for specialization
  generic[n: NEURONS]: MODULE = 
  BEGIN
    INPUT i: SIGS 	% effect on input signal: amount to go up/down in response to input
    OUTPUT o: BOOLEAN
    OUTPUT level: LEVELS
    LOCAL sens: [1 .. 2]
    LOCAL pir: BOOLEAN
   INITIALIZATION
    pir = FALSE;
    level = 0
   DEFINITION
    sens = IF (n = Z) THEN 1 ELSE 2 ENDIF; % sensitivity of neuron to inputs
    o = (level = N) 	% outs[B31] will not be used anyway
   TRANSITION
    [
     FIRE: level = N AND GNEURONS(n) AND NOT(pir) --> 
	level' = N - 2*sens 	% Ignore input signal, just fire
     []
     level < N AND i' = pos --> 
 	level' = IF (level > N - sens) THEN N ELSE level + sens ENDIF
     []
     (NOT(GNEURONS(n)) OR level < N) AND i' = neg --> 
 	level' = IF (level > 1) THEN level - 2 ELSE 0 ENDIF
     []
     n = B52 AND level = 0 AND i = neg AND i' = neg --> 	% Non-det PIR
	pir' = TRUE;
 	level' = N
     []
     % n = B52 AND level = N AND pir included below
     ELSE --> 		% too short time to notice effect of decay
    ]
  END;

  aplysia_neurons: MODULE = 
    (WITH INPUT ins: ARRAY NEURONS OF SIGS
     WITH OUTPUT outs: ARRAY NEURONS OF BOOLEAN
     WITH OUTPUT levels: ARRAY NEURONS OF LEVELS
      (|| (n: NEURONS): (RENAME o to outs[n], i to ins[n], level to levels[n] IN generic[n])));


  %-----------------------
  %  Minimum of an array
  %-----------------------

  diff(x1: LEVELS, x2: LEVELS): SIGS = 
    IF (x1 > x2) THEN pos ELSIF (x1 < x2) THEN neg ELSE zero ENDIF;

  negate(x: BOOLEAN): SIGS = IF x THEN neg ELSE zero ENDIF;

  map(x: BOOLEAN): SIGS = IF x THEN pos ELSE zero ENDIF;

  count(x1: SIGS, nums: ARRAY [0 .. 1] OF [0 .. 7]): ARRAY [0 .. 1] OF [0 .. 7] = 
    IF (x1 = pos) 
    THEN [ [i: [0 .. 1]] IF i=0 THEN nums[i]+1 ELSE nums[i] ENDIF ]
    ELSIF (x1 = neg)
    THEN [ [i: [0 .. 1]] IF i=1 THEN nums[i]+1 ELSE nums[i] ENDIF ]
    ELSE nums ENDIF;

  integrate(x1: SIGS, x2: SIGS, x3: SIGS, x4: SIGS, x5: SIGS, x6: SIGS, x7: SIGS): SIGS = 
    LET 
     c: ARRAY [0 .. 1] OF [0 .. 7] = count(x1, count(x2, count(x3, count(x4, count(x5, count(x6, count(x7, [ [i:[0 .. 1]] 0])))))))
    IN
      IF (c[0] > c[1]) THEN pos
      ELSIF (c[1] > c[0]) THEN neg
      ELSE zero ENDIF;

  integrate31(x1: SIGS, x2: SIGS, x3: SIGS, x4: SIGS, x5: SIGS, x6: SIGS, x7: SIGS): SIGS = 
    LET ans:SIGS = integrate(x1, x2, x3, x4, x5, x6, x7) IN
      IF (ans = neg AND x1=neg) THEN neg
      ELSIF (ans = neg) THEN zero ELSE ans ENDIF;
      
  integrate64(x1: SIGS, x2: SIGS, x3: SIGS, x4: SIGS, x5: SIGS, x6: SIGS, x7: SIGS): SIGS = 
    IF x1=pos THEN pos
    ELSIF x2=neg THEN neg
    ELSE zero ENDIF;		% integrate(x1,x2,x3,x4,x5,x6,x7)

  integrate8(x1: SIGS, x2: SIGS, x3: SIGS, x4: SIGS, x5: SIGS, x6: SIGS, x7: SIGS): SIGS = 
    IF x5=pos THEN pos ELSE integrate(x1,x2,zero,x4,x5,x6,x7) ENDIF;

  integrate51(x1: SIGS, x2: SIGS, x3: SIGS, x4: SIGS, x5: SIGS, x6: SIGS, x7: SIGS): SIGS = 
    IF (x1=neg OR x2=neg OR x3=neg) THEN neg
    ELSE integrate(x1,x2,x3,x4,zero,x6,x7) ENDIF;

  % ADD INITIAL CURRENT INPUT
  aplysia_wiring: MODULE =
   BEGIN
    INPUT b63i: SIGS
    INPUT outs: ARRAY NEURONS OF BOOLEAN
    OUTPUT ins: ARRAY NEURONS OF SIGS
    INPUT levels: ARRAY NEURONS OF LEVELS
   INITIALIZATION
    ins = [ [i: NEURONS] zero ]
    % ins = [ [i: NEURONS] IF (i = B31) THEN pos ELSE zero ENDIF ]
   TRANSITION
    [
     TRUE -->
	ins' = [ [n: NEURONS] 
        LET 
	ec: [[NEURONS,NEURONS]->SIGS] = LAMBDA(a,b:NEURONS): diff(levels[a],levels[b]),
        ip:[NEURONS->SIGS] = LAMBDA(x:NEURONS): negate(outs[x]),
        ep:[NEURONS->SIGS] = LAMBDA(x:NEURONS): map(outs[x]) IN
	IF(n = B31) THEN
		integrate31(ip(B64),ep(B34),ep(B63),ep(B35),ep(B4),ec(B63,B31),ec(B35,B31))
	ELSIF(n = B34) THEN 
		integrate(ep(B63),ip(B64),zero,zero,zero,zero,zero)
	ELSIF(n = B63) THEN 
		integrate(ip(B64),ec(B31,B63),ep(B34),zero,zero,zero,b63i)
	ELSIF (n = B35) THEN 
		integrate(ip(B64),ec(B31,B35),ip(B52),zero,zero,zero,zero)
	ELSIF (n = B64) THEN 
		integrate64(ep(Z),ip(B52),ip(B34),ip(B63),ip(B4),ep(B51),ec(B51,B64))
	ELSIF (n = B4) THEN 
		integrate(ip(B52),ep(B35),ec(B51,B4),ep(B64),zero,zero,zero)
	ELSIF (n = B51) THEN 
		integrate51(ip(B35),ip(B52),ip(B4),ec(B64,B51),ec(B4,B51),zero,zero)
	ELSIF (n = B52) THEN 
		integrate(ep(B35),ip(B64),ip(B51),ip(B4),zero,zero,zero)
	ELSIF (n = B8) THEN 
		integrate8(ep(B51),ip(B52),ip(B63),ip(B4),ep(B34),zero,zero)
	ELSE integrate(ep(B63),zero,zero,zero,zero,zero,zero) ENDIF ]
    ]
   END;

  observer: MODULE = 
  BEGIN
    OUTPUT b63i: SIGS		% generate the input signal b63i
    INPUT levels: ARRAY NEURONS OF LEVELS
    OUTPUT phase: PHASES
  INITIALIZATION
    b63i = pos
  DEFINITION 
    phase = IF (b63i = pos OR levels[B63]=N OR levels[B35]=N OR levels[B31]=N OR levels[B34]=N)
	    THEN protraction
	    ELSIF (levels[B64]=N OR levels[B4]=N) THEN retraction
	    ELSE termination ENDIF
  TRANSITION
    [ levels[B35]=N --> b63i' = zero
    []
    ELSE --> ]
  END;

  aplysia: MODULE = aplysia_wiring || aplysia_neurons || observer ;

   %--------------
   %  Properties 
   %--------------

   %allzero: THEOREM
      %aplysia |-  G(b63i = zero) => G(FORALL (i: NEURONS): outs[i] = FALSE);

   % Protraction phase
   p0: THEOREM
      aplysia |- U(b63i = pos, U(b63i = zero, phase = retraction));

   p1: THEOREM
      aplysia |- F( levels[B31] = N AND U(levels[B31] >= N-1, phase = retraction) );
      % aplysia |- G( b63i = pos => G(F(levels[B31] >= N-1)) );

   p2: THEOREM
      aplysia |- U( F(levels[B34] = N), X(X(levels[B64] = N)) );
      %aplysia |- G( b63i = pos => G(F(levels[B34] = N)) );

   p3: THEOREM
      aplysia |- U( F(levels[B35] = N), X(X(phase = retraction)) );
      %aplysia |- G( b63i = pos => G(F(levels[B35] = N)) );

   p4: THEOREM
      aplysia |- F(phase = protraction AND levels[B8] = N);

   % Transition phase
   t1: THEOREM
      aplysia |- F( levels[Z] = N );

   t2: THEOREM
      aplysia |- F( b63i = zero AND levels[B64] = N );

   t3: THEOREM
      aplysia |- F( b63i = zero AND levels[B64] = N AND G( levels[B63] < N ) );

   t4: THEOREM
      aplysia |- F( phase = retraction AND levels[B64] = N );

   % Retraction phase
   r0: THEOREM
      aplysia |- G( phase = retraction => levels[B64] = N );

   r1: THEOREM
      aplysia |- G( phase = retraction => levels[B35] < N );

   r2: THEOREM
      aplysia |- G( phase = retraction => levels[B34] < N );

   % eventually termination is not true, ...
   r3: THEOREM
      aplysia |- W( F( levels[B4] = N ), X(X(phase = termination)));
      %aplysia |- G(F( levels[B4] = N OR phase = termination ));

   r4: THEOREM
      aplysia |- G( levels[B51] < N );

   r5: THEOREM
      aplysia |- G( phase /= protraction => levels[B8] < N );

   % termination phase
   e1: THEOREM 
      aplysia |- G( phase = termination => F(G( levels[B64] = 0 )) );

   e2: THEOREM
      aplysia |- U( phase = protraction, phase /= protraction );

   e3: THEOREM
      aplysia |- U( phase = protraction, W(phase = retraction, phase = termination) );

   % special case of e3
   e4: THEOREM
      aplysia |- G( phase = termination => G( phase = termination ) );

   e5: THEOREM
      % aplysia |- G(( phase = termination AND levels[B31] = 0) => G( phase = termination AND levels[B31] = 0 AND levels[B63] = 0 AND levels[B35] = 0) );
      aplysia |- G(( phase = termination ) => G( phase = termination AND levels[B31] < N AND levels[B63] < N AND levels[B35] < N) );

   e6: THEOREM
      aplysia |- G( phase = termination => F(G( levels[B64] = 0 AND levels[B4] = 0 ) ));

END