MODULE main

VAR
  seisu : 1..1000;
  prt   : {OK, NG};

ASSIGN
  init(seisu) := 1;
  next(seisu) := {1..1000};

  init(prt) := NG;
  next(prt) :=
    case
      (seisu mod 6) = 0 : OK;
      TRUE              : NG;
    esac;

SPEC AG ( ( ( seisu mod 6) = 0) -> AX(prt = OK))
SPEC AG (!((seisu mod 6) = 0) -> AX(prt = NG))