uni/fmi/fmi23block4/ex2.b.smv

MODULE main
VAR
  pc: { L0, L1, L2, L3, L4, L5, L6, L7, L8 };
  year: unsigned word [11];
  days: unsigned word [14];
DEFINE
  is_leap_year := (toint(year) mod 4 = 0 & toint(year) mod 100 != 0) |
                  (toint(year) mod 400 = 0);
ASSIGN
  init(pc) := L0;
  next(pc) :=
    case
      pc = L0 : L1;
      pc = L1 & days > 0ud14_365 : L2;
      pc = L1 : L8;
      pc = L2 & is_leap_year : L3;
      pc = L2 : L6;
      pc = L3 & days > 0ud14_366 : L4;
      pc = L3 : L1;
      pc = L4 : L5;
      pc = L5 : L1;
      pc = L6 : L7;
      pc = L7 : L1;
      -- self-loop at final location L8, to obtain infinite paths
      pc = L8 : L8;
    esac;
  next(year) :=
    case
      pc = L0 : 0ud11_1980;
      pc = L5 : year + 0ud11_1;
      pc = L7 : year + 0ud11_1;
      TRUE: year;
    esac;
  next(days) :=
    case
      -- in case we are at line 4, we subtract 366 days (with a unsigned 14-bit constant)
      pc = L4 : days - 0ud14_366;
      -- in case we are at line 4, we subtract 365 days (with a unsigned 14-bit constant)
      pc = L6 : days - 0ud14_365;
      TRUE : days;
    esac;

-- we enter the loop with PC being L1 (which is a consequence of PC being L0)
-- all executions will start at L0 and end up in L1, so we could optimize away the premise of the implication, but we still want to implement the expressed property
-- if the premise is fulfilled, then for all execution paths sometime in the future the PC must reach L8, which is the line where the loop has been exited
SPEC AG (pc = L1 -> AF (pc = L8))

-- out of curiosity we also verify include the optimized property
--SPEC AF (pc = L8)
-- it gives the same output!