--- test OCC native binding

(reset)
in ../lib/native.msr

(
module nativetest
import native * .

clock: nat -> state.

START, FINISHED, TIMEOUT: state.

A, B: princ.

initiator: for A. {
  exists L: nat -> nonce -> state.
  
  send:
  forall time: nat.
     clock time;
     START
  => exists nA: nonce.
     A & B & nA,
     L time nA.
     
  receive:
  forall time: nat.
  forall time2: nat.
  forall nA: nonce.
     clock time2 ;
     B & A & nA,
     L time nA
  => FINISHED
     if le time2 (plus time 2).
  
  timeout:
  forall time: nat.
  forall time2: nat.
  forall nA: nonce.
     clock time2 ;
     not (le time2 (plus time 2)) ;
     L time nA
  => TIMEOUT .
}

responder: for B. {
  answer:
  forall nA: nonce.
     A & B & nA
  => B & A & nA.
}

advance_clock: for A. {
  tick:
    forall n: nat.
    clock n => clock (plus n 1).
}
)