// -----------------------------------------------------------------
//
// System.txt
// RISCAL specifiation of a client-server system
//
// (c) 2020, Wolfgang Schreiner: Thinking Programs
// 
// -----------------------------------------------------------------
 
val N = 3;
axiom notNull ⇔ N > 0;
 
type Client = ℕ[N-1];
type Client0 = ℕ[N];
type PC = ℕ[2];
type PCs = Map[Client,PC];

type State = Record[
  given: Client0,
  waiting: Set[Client],
  pc: PCs,
  req: Set[Client],
  ans: Set[Client]
];
 
pred I(s:State) ⇔
  s.given = N ∧
  s.waiting = ∅[Client] ∧
  s.pc = Map[Client,PC](0) ∧
  s.req = ∅[Client] ∧
  s.ans = ∅[Client]
;

// -----------------------------------------------------------------
// relational system model
// -----------------------------------------------------------------

pred Goto(i:Client,from:PC,to:PC,pc:PCs,pc0:PCs) ⇔
  pc[i] = from ∧ pc0 = pc with [i] = to;
pred Send(value:Client, channel:Set[Client], channel0:Set[Client]) ⇔
  ¬(value ∈ channel) ∧ channel0 = channel∪{value};
pred Receive(value:Client, channel:Set[Client], channel0:Set[Client]) ⇔
  value ∈ channel ∧ channel0 = channel\{value};
  
pred RC(i:Client,s:State,s0:State) ⇔
  s0.given = s.given ∧ s0.waiting = s.waiting ∧
  (
    (Goto(i,0,1,s.pc,s0.pc) ∧ Send(i,s.req,s0.req) ∧ s0.ans = s.ans) ∨
    (Goto(i,1,2,s.pc,s0.pc) ∧ Receive(i,s.ans,s0.ans) ∧ s0.req = s.req) ∨
    (Goto(i,2,0,s.pc,s0.pc) ∧ Send(i,s.req,s0.req) ∧ s0.ans = s.ans)
  )
;

pred RS(i:Client,s:State,s0:State) ⇔
  Receive(i,s.req,s0.req) ∧ s0.pc = s.pc ∧
  (
    (i = s.given ∧ s.waiting = ∅[Client] ∧
      s0.given = N ∧ s0.waiting = s.waiting ∧ s0.ans = s.ans) ∨
    (i = s.given ∧ ∃g∈s.waiting. 
      (s0.given = g ∧ s0.waiting = s.waiting\{g} ∧ Send(s0.given, s.ans, s0.ans))) ∨
    (i ≠ s.given ∧ s.given = N ∧
      s0.given = i ∧ s0.waiting = s.waiting ∧ Send(s0.given, s.ans, s0.ans)) ∨
    (i ≠ s.given ∧ s.given ≠ N ∧
      s0.waiting = s.waiting∪{i} ∧ s0.given = s.given ∧ s0.ans = s.ans)
  );
   
pred R(s:State, s0:State) ⇔ ∃i:Client. RC(i,s,s0) ∨ RS(i,s,s0);
  
// -----------------------------------------------------------------
// functional system model
// -----------------------------------------------------------------

rectype(0) Action =
  Request(Client) | Get(Client) | Return(Client) |
  Return1(Client) | Return2(Client,Client) | 
  Request1(Client) | Request2(Client);
  
pred enabled(a:Action,s:State) ⇔
  match a with
  {
    Request(i:Client) -> 
      s.pc[i] = 0 ∧ ¬(i ∈ s.req);
    Get(i:Client) -> 
      s.pc[i] = 1 ∧ i ∈ s.ans;
    Return(i:Client) -> 
      s.pc[i] = 2 ∧ ¬(i ∈ s.req);
    Return1(i:Client) -> 
      i ∈ s.req ∧ i = s.given ∧ s.waiting = ∅[Client];
    Return2(i:Client,g:Client) -> 
      i ∈ s.req ∧ i = s.given ∧ g ∈ s.waiting ∧ ¬(g ∈ s.ans);
    Request1(i:Client) -> 
      i ∈ s.req ∧ i ≠ s.given ∧ s.given = N ∧ ~(i ∈ s.ans);
    Request2(i:Client) -> 
      i ∈ s.req ∧ i ≠ s.given ∧ s.given ≠ N;
  }
;

fun execute(a:Action,s:State):State =
  match a with
  {
    Request(i:Client) -> 
      s with .pc = (s.pc with [i] = 1) with .req = s.req∪{i};
    Get(i:Client) -> 
      s with .pc = (s.pc with [i] = 2) with .ans = s.ans\{i};
    Return(i:Client) -> 
      s with .pc = (s.pc with [i] = 0) with .req = s.req∪{i};
    Return1(i:Client) -> 
      s with .req = s.req\{i} with .given = N;
    Return2(i:Client,g:Client) -> 
      s with .req = s.req\{i} with .given = g 
        with .waiting = s.waiting\{g} with .ans = s.ans∪{g};
    Request1(i:Client) -> 
      s with .req = s.req\{i} with .given = i with .ans = s.ans∪{i};
    Request2(i:Client) -> 
      s with .req = s.req\{i} with .waiting = s.waiting∪{i};
  }
;

// -----------------------------------------------------------------
// equivalence of the models
// -----------------------------------------------------------------

theorem Equiv(s:State) ⇔
  ∀s0:State. R(s,s0) ⇔ ∃a:Action. enabled(a,s) ∧ s0 = execute(a,s);

// -----------------------------------------------------------------
// checking mutual exclusion of the model
// -----------------------------------------------------------------

pred MutEx(s:State) ⇔ ∀i:Client,j:Client with i≠j. ¬(s.pc[i] = 2 ∧ s.pc[j] = 2);

val S = 80;
proc System(s:State):()
  requires I(s);
{
  var s0:State = s;
  assert MutEx(s0);
  var trace:Array[S+1,State] = Array[S+1,State](s0);
  var i:ℕ[S] ≔ 0; 
  while i < S ∧ ∀j:ℕ[S] with j<i. trace[j] ≠ trace[i] do
  {
    choose s1:State with R(s0,s1);
    // choose a:Action with enabled(a,s0);
    // val s1:State ≔ execute(a,s0);
    trace[i+1] ≔ s1;
    assert MutEx(s1) ∨ print i,trace in ⊥;
    s0 ≔ s1;
    i:= i+1;
  }
  assert i < S-1;
}

proc System0(s:State):()
  requires I(s);
{
  assert MutEx(s);
  var old: Set[State] = {s};
  var new: Set[State];
  do
  {
    // new ≔ { s1 | s1:State with ∃s0∈old. R(s0,s1) };
    new ≔ { execute(a,s) | a:Action,s∈old with enabled(a,s) };
    new ≔ new\old;
    assert ∀s∈new. MutEx(s);
    old ≔ old ∪ new;
  }
  while new ≠ ∅[State];
}

val T = 10;
type Trace = Array[T,Action];
type Elem = Tuple[ℕ[T],Trace,State];

proc System1(s:State):()
  requires I(s);
{
  assert MutEx(s);
  var trace:Trace = Array[T,Action](Action!Request(0));
  var old: Set[Elem] = {⟨0,trace,s⟩};
  var new: Set[Elem];
  do
  {
    new ≔ { ⟨s.1+1,s.2 with [s.1]=a,execute(a,s.3)⟩ | 
      a:Action,s∈old with enabled(a,s.3) };
    new ≔ { s | s∈new with ∀s0∈old. (s.3 ≠ s0.3) };
    assert ∀s∈new. MutEx(s.3);
    old ≔ old ∪ new;
  }
  while new ≠ ∅[Elem];
}
  
// -----------------------------------------------------------------
// invariant-based verification of mutual exclusion
// -----------------------------------------------------------------

pred Invariant(s:State) ⇔ 
  ∀i:Client.
    (i = s.given ⇒
      (s.pc[i] = 0 ∧ i ∈ s.req) ∨
      (s.pc[i] = 1 ∧ i ∈ s.ans) ∨ 
      (s.pc[i] = 2 ∧ ¬(i ∈ s.req) ∧ ¬(i ∈ s.ans))) ∧ 
    (i ∈ s.waiting ⇒
      i ≠ s.given ∧ s.pc[i] = 1 ∧ ¬(i ∈ s.req) ∧ ¬(i ∈ s.ans)) ∧
    (i ∈ s.req ⇒ ¬(i ∈ s.ans)) ∧
    (i ∈ s.ans ⇒ s.given = i) ∧
    (s.pc[i] = 0 ⇒ ¬(i ∈ s.ans) ∧
      (i ∈ s.req ⇒ i = s.given)) ∧
    (s.pc[i] = 1 ⇒ 
      i ∈ s.req ∨ i ∈ s.waiting ∨ i ∈ s.ans) ∧
    (s.pc[i] = 2 ⇒ i = s.given)
;

theorem MutEx0(s:State) ⇔ 
  Invariant(s) ⇒ MutEx(s);
theorem MutEx1(s:State) ⇔ 
  I(s) ⇒ Invariant(s);
theorem MutEx2(s:State,s0:State) ⇔ 
  Invariant(s) ∧ R(s,s0) ⇒ MutEx(s0);
theorem MutEx2(s:State) ⇔ 
  Invariant(s) ⇒
    ∀a:Action with enabled(a,s). 
      let s0 = execute(a,s) in Invariant(s0);

// -----------------------------------------------------------------
// end of file
// -----------------------------------------------------------------