MODULE Miesiac (typ_roku)
VAR miesiac : {styczen, luty, marzec, kwiecien, maj, czerwiec, lipiec, sierpien, wrzesien, pazdziernik, listopad, grudzien};
VAR dzien : 1..32;
VAR maxDni : 28..31;
ASSIGN
init(miesiac) := styczen;
next(miesiac) := case
miesiac = styczen & dzien = maxDni : luty;
miesiac = luty & dzien = maxDni: marzec;
miesiac = marzec & dzien = maxDni: kwiecien;
miesiac = kwiecien & dzien = maxDni: maj;
miesiac = maj & dzien = maxDni: czerwiec;
miesiac = czerwiec & dzien = maxDni: lipiec;
miesiac = lipiec & dzien = maxDni: sierpien;
miesiac = sierpien & dzien = maxDni: wrzesien;
miesiac = wrzesien & dzien = maxDni: pazdziernik;
miesiac = pazdziernik & dzien = maxDni: listopad;
miesiac = listopad & dzien = maxDni: grudzien;
miesiac = grudzien & dzien = maxDni: styczen;
TRUE : miesiac;
esac;
init(dzien) := 1;
next(dzien) := case
((dzien + 1) <= maxDni) : dzien + 1;
TRUE: 1;
esac;
init(maxDni) := 31;
next(maxDni) := case
next(miesiac) = styczen & dzien = maxDni: 31;
next(miesiac) = luty & typ_roku = normalny & dzien = maxDni: 28;
next(miesiac) = luty & typ_roku = przestepny & dzien = maxDni: 29;
next(miesiac) = marzec & dzien = maxDni: 31;
next(miesiac) = kwiecien & dzien = maxDni: 30;
next(miesiac) = maj & dzien = maxDni: 31;
next(miesiac) = czerwiec & dzien = maxDni: 30;
next(miesiac) = lipiec & dzien = maxDni: 31;
next(miesiac) = sierpien & dzien = maxDni: 31;
next(miesiac) = wrzesien & dzien = maxDni: 30;
next(miesiac) = pazdziernik & dzien = maxDni: 31;
next(miesiac) = listopad & dzien = maxDni: 30;
next(miesiac) = grudzien & dzien = maxDni: 31;
TRUE : maxDni;
esac;