IEEE 802.11 Wireless LAN

// Modest model of IEEE 802.11 Wireless LAN
action send, send1, send2;
action finish, finish1, finish2;
action success, success1, success2;
action bck, bck1, bck2;
action coll1, coll2;

const int BCMAX = 2;

// Parameters for the physical layer
const int ASLOT = 1;
const int DIFS = 3; // due to scaling can be non-deterministically either 2 or 3
const int VULN = 1; // due to scaling can be non-deterministically either 0 or 1
const int TTMAX = 315; // scaling up // 25 for deadlines & expected
const int TTMIN = 4; // scaling down
const int ACK_TO = 6;
const int ACK = 4; // due to scaling can be non-deterministically either 3 or 4
const int SIFS = 1; // due to scaling can be non-deterministically either 0 or 1

// packet status
// 0: nothing sent
// 1: sending correctly
// 2: sending garbled
int c1 limit [0..2]; // first station's packet
int c2 limit [0..2]; // second station's packet


// Properties
// Probabilistic reachability
const int K = 2;
// "with probability 1, eventually both stations have sent their packet correctly"
property P_1 = P(<> did(success1) && did(success2)) >= 1.0;
// "the maximum probability that either station's backoff counter reaches K"
property P_max = Pmax(<> did(bck1) || did(bck2));

// Time-bounded probabilistic reachability
const int DEADLINE = 100;
// "the minimum probability of both stations correctly
//  delivering their packets within time DEADLINE"
property D_and = Pmin(<> did(success1) && did(success2) && time <= DEADLINE);
// "the minimum probability of either station correctly
//  delivering its packet within time DEADLINE"
property D_or = Pmin(<> (did(success1) || did(success2)) && time <= DEADLINE);
// "the minimum probability of station 1 correctly
//  delivering its packet within time DEADLINE"
property D_1 = Pmin(<> did(success1) && time <= DEADLINE);

// Expected reachability
// "the maximum expected time until both stations correctly deliver their packets"
property E_and = Tmax(did(success1) && did(success2));
// "the maximum expected time until either station correctly delivers its packet"
property E_or = Tmax(did(success1) || did(success2));
// "the maximum expected time until station 1 correctly delivers its packet"
property E_1 = Tmax(did(success1));


process Channel()
{
   do {
      :: finish1 {= c1 = 0 =}
      :: finish2 {= c2 = 0 =}
      :: send1 {= c1 = min(c2 + 1, 2), c2 = min(c2 + c2, 2) =}
      :: send2 {= c1 = min(c1 + c1, 2), c2 = min(c1 + 1, 2) =}
   }
}

process Sender(int id limit [1..2])
{
   clock x;
   int status limit [0..2];
   int bc limit [0..BCMAX];
   int backoff limit [0..pow(2, BCMAX + 4) - 1];

   process SENSE()
   {
      invariant(x <= DIFS)
      alt {
         :: when(x == DIFS || x == DIFS - 1) {= x = 0 =};
            VULN()
         :: when(c1 + c2 > 0) urgent(c1 + c2 > 0) {= x = 0 =};
            WAIT_FREE()
      }
   }

   process VULN()
   {
      invariant(x <= VULN)
      when(x == VULN || x == VULN - 1) send {= x = 0 =};
      TRANSMIT()
   }

   process TRANSMIT()
   {
      invariant(x <= TTMAX)
      alt {
         :: when(id == 1 && x >= TTMIN) finish {= x = 0, status = c1 =};
            TEST_CHAN()
         :: when(id == 2 && x >= TTMIN) finish {= x = 0, status = c2 =};
            TEST_CHAN()
      }
   }

   process TEST_CHAN()
   {
      urgent
      alt {
         :: when(c1 + c2 > 0) tau;
            WAIT_FREE()
         :: when(c1 + c2 == 0 && status == 2) tau;
            NO_ACK()
         :: when(c1 + c2 == 0 && status == 1) tau;
            SEND_ACK()
      }
   }

   process SEND_ACK()
   {
      invariant(x <= SIFS)
      when(x == SIFS || x == SIFS - 1) send {= x = 0 =};
      ACK()
   }

   process ACK()
   {
      invariant(x <= ACK)
      when(x == ACK || x == ACK - 1) finish {= x = 0 =};
      urgent success // DONE
   }

   process NO_ACK()
   {
      invariant(x <= ACK_TO)
      when(x == ACK_TO) {= x = 0 =};
      WAIT_DIFS()
   }

   process WAIT_FREE()
   {
      when(c1 + c2 == 0) urgent(c1 + c2 == 0) {= x = 0 =};
      WAIT_DIFS()
   }

   process WAIT_DIFS()
   {
      invariant(x <= DIFS)
      alt {
         :: when((x == DIFS || x == DIFS - 1))
            {= backoff = DiscreteUniform(0, pow(2, bc + 4) - 1),
               bc = min(bc + 1, BCMAX), x = 0 =};
            // The following line is only for reachability properties
            urgent alt { :: when(bc == K) bck :: when(bc != K) tau };
            BACKOFF()
         :: when(c1 + c2 > 0) urgent(c1 + c2 > 0) {= x = 0 =};
            WAIT_FREE()
      }
   }

   process BACKOFF()
   {
      invariant(x <= ASLOT)
      alt {
         :: when(x == ASLOT && backoff == 0) {= x = 0 =};
            VULN()
         :: when(x == ASLOT && backoff > 0) {= backoff = backoff - 1, x = 0 =};
            BACKOFF()
         :: when(c1 + c2 > 0) urgent(c1 + c2 > 0) {= x = 0 =};
            WAIT_FREEII()
      }
   }

   process WAIT_FREEII()
   {
      when(c1 + c2 == 0) urgent(c1 + c2 == 0) {= x = 0 =};
      WAIT_DIFSII()
   }

   process WAIT_DIFSII()
   {
      invariant(x <= DIFS)
      alt {
         :: when(x == DIFS || x == DIFS - 1) {= x = 0 =};
            BACKOFF()
         :: when(c1 + c2 > 0) urgent(c1 + c2 > 0) tau;
            WAIT_FREEII()
      }
   }

   SENSE()
}


par {
   :: Channel()
   :: relabel {send, finish, success, bck}
      by {send1, finish1, success1, bck1} Sender(1)
   :: relabel {send, finish, success, bck}
      by {send2, finish2, success2, bck2} Sender(2)
}