uni/fmi/fmi23block4/ex2.c.smv

MODULE main
VAR
  pc: { L0, L1, L2, L3, L4 };
  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);
  days_in_year := is_leap_year ? 0ud14_366 : 0ud14_365;
ASSIGN
  init(pc) := L0;
  next(pc) :=
    case
      pc = L0 : L1;
      pc = L1 & days > days_in_year : L2;
      pc = L1 : L4;
      pc = L2 : L3;
      pc = L3 : L1;
      -- self-loop at final location L4, to obtain infinite paths
      pc = L4 : L4;
    esac;
  next(year) :=
    case
      pc = L0 : 0ud11_1980;
      -- we compacted the program to just one addition branch on year
      pc = L3 : year + 0ud11_1;
      TRUE: year;
    esac;
  next(days) :=
    case
      -- we compacted the program to just one subtraction branch on days
      pc = L2 : days - days_in_year;
      TRUE : days;
    esac;

-- for completeness, here is the program we are modeling in this version
-- it is the legendary readable and compact solution provided by Stefan Ciobaca
-- in our case we don't need any inlined functions :)
-- L0:   year = ORIGIN_YEAR;
-- L1:       while (days > DaysInYear(year)) {
-- L2:       days -= DaysInYear(year);
-- L3:       year++;
--       }
-- L4:   exit;

-- our specification remains the same as in subtask (b), only this time our exit PC is L4
SPEC AG (pc = L1 -> AF (pc = L4))

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