// -------------------------------------------------------------------------
// a bit transmission protocol
// (c) 2024, Wolfgang Schreiner <Wolfgang.Schreiner@risc.jku.at>
// -------------------------------------------------------------------------

// the types
type Bit = ℕ[1];
type PC1 = ℕ[2];
type PC2 = ℕ[1];

// an operational description of the system
shared system Bits
{
  // the local variables
  var x:Bit; var y:Bit;
  
  // the wires
  var v:Bit = 0; var r:Bit = 0; var a:Bit = 0;
  
  // the program counters
  var p:PC1 = 0; var q:PC2 = 0;
  
  // the correctness property
  invariant q = 1 ⇒ y = x;
  
  // the system invariants that imply the correctness property
  invariant p = 0 ⇒ q = 0 ∧ r = 0 ∧ a = 0;
  invariant p = 1 ⇒ r = 1 ∧ v = x;
  invariant p = 2 ⇒ r = 0;
  invariant q = 0 ⇒ a = 0;
  invariant q = 1 ⇒ (p = 1 ∨ p = 2) ∧ a = 1 ∧ y = x;

  // the non-deterministically chosen initial state values
  init (x0:Bit, y0:Bit) { x ≔ x0; y ≔ y0; }
  
  // the sender actions
  action S1(any:Bit) with p = 0;
  {
    x ≔ any; v ≔ x; r ≔ 1; p ≔ 1;
  }
  action S2() with p = 1 ∧ a = 1;
  {
    r ≔ 0; p ≔ 2;
  }
  action S3() with p = 2 ∧ a = 0;
  {
    p ≔ 0;
  }
  
  // the receiver actions
  action R1() with q = 0 ∧ r = 1;
  {
    y ≔ v; a ≔ 1; q = 1;
  }
  action R2() with q = 1 ∧ r = 0;
  {
    a ≔ 0; q ≔ 0;
  }
}

// -------------------------------------------------------------------------
// a declarative (logical) description of the system below
// -------------------------------------------------------------------------

// the initial state condition
pred Init(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2) ⇔
  v = 0 ∧ r = 0 ∧ a = 0 ∧ p = 0 ∧ q = 0;
  
// the transition relations
pred S1(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
        x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  p = 0 ∧ p0 = 1 ∧ v0 = x0 ∧ r0 = 1 ∧ // x0 arbitrary
  q0 = q ∧ y0 = y ∧ a0 = a;
pred S2(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
        x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  p = 1 ∧ p0 = 2 ∧ a = 1 ∧ r0 = 0 ∧
  q0 = q ∧ x0 = x ∧ y0 = y ∧ v0 = v ∧ a0 = a;
pred S3(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
        x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  p = 2 ∧ p0 = 0 ∧ a = 0 ∧ 
  q0 = q ∧ x0 = x ∧ y0 = y ∧ v0 = v ∧ r0 = r ∧ a0 = a;
pred R1(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
        x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  q = 0 ∧ q0 = 1 ∧ r = 1 ∧ y0 = v ∧ a0 = 1 ∧
  p0 = p ∧ x0 = x ∧ v0 = v ∧ r0 = r;
pred R2(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
        x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  q = 1 ∧ q0 = 0 ∧ r = 0 ∧ a0 = 0 ∧ 
  p0 = p ∧ x0 = x ∧ y0 = y ∧ v0 = v ∧ r0 = r;
  
// the invariant
pred Invariant(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2) ⇔
  (p = 0 ⇒ q = 0 ∧ r = 0 ∧ a = 0) ∧
  (p = 1 ⇒ r = 1 ∧ v = x) ∧
  (p = 2 ⇒ r = 0) ∧
  (q = 0 ⇒ a = 0) ∧
  (q = 1 ⇒ (p = 1 ∨ p = 2) ∧ a = 1 ∧ y = x); 
  
// the correctness property
pred Property(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2) ⇔
  q = 1 ⇒ y = x;
  
// the verification conditions
theorem VC0(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2) ⇔
  Init(x,y,v,r,a,p,q) ⇒ Property(x,y,v,r,a,p,q);
theorem VC1(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
  x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  Invariant(x,y,v,r,a,p,q) ∧ S1(x,y,v,r,a,p,q,x0,y0,v0,r0,a0,p0,q0) ⇒
    Invariant(x0,y0,v0,r0,a0,p0,q0);  
theorem VC2(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
  x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  Invariant(x,y,v,r,a,p,q) ∧ S2(x,y,v,r,a,p,q,x0,y0,v0,r0,a0,p0,q0) ⇒
    Invariant(x0,y0,v0,r0,a0,p0,q0);
theorem VC3(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
  x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  Invariant(x,y,v,r,a,p,q) ∧ S3(x,y,v,r,a,p,q,x0,y0,v0,r0,a0,p0,q0) ⇒
    Invariant(x0,y0,v0,r0,a0,p0,q0); 
theorem VC4(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
  x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  Invariant(x,y,v,r,a,p,q) ∧ R1(x,y,v,r,a,p,q,x0,y0,v0,r0,a0,p0,q0) ⇒
    Invariant(x0,y0,v0,r0,a0,p0,q0); 
theorem VC5(x:Bit,y:Bit,v:Bit,r:Bit,a:Bit,p:PC1,q:PC2,
  x0:Bit,y0:Bit,v0:Bit,r0:Bit,a0:Bit,p0:PC1,q0:PC2) ⇔
  Invariant(x,y,v,r,a,p,q) ∧ R2(x,y,v,r,a,p,q,x0,y0,v0,r0,a0,p0,q0) ⇒
    Invariant(x0,y0,v0,r0,a0,p0,q0);

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

