Hi,
I am new in TLA+, I want to write specification in TLA+ but the issue is I am confused about the tool TLC.
My specification is as follows (without keeping in view the syntax just sharing you the logic)
For example:
---------------------------------------------------------------------
Constant Month, Day
if Month \in 1,3,5,7,8,10,12 then
1<Day<31
else
1<Day<30
end if
----------------------------------------------------------------------
Above is the specification but I am confused in Model where should i write this.
Please do share the understanding or difference between these, if possible.
But still confused.
Thanks,
Malaika