mirror of
https://github.com/johndoe6345789/tustu.git
synced 2026-04-24 13:45:00 +00:00
26 lines
456 B
INI
26 lines
456 B
INI
\* TLA+ Configuration file for RegistrationKey specification
|
|
|
|
CONSTANTS
|
|
MAX_STRING_LENGTH = 50
|
|
ASCII_MIN = 32
|
|
ASCII_MAX = 122
|
|
|
|
SPECIFICATION Spec
|
|
|
|
INVARIANTS
|
|
TypeInvariant
|
|
ValidInputs
|
|
PhaseOrder
|
|
FinalKeyLength
|
|
NoEmptyKey
|
|
|
|
PROPERTIES
|
|
Termination
|
|
|
|
\* Constraint to limit state space for model checking
|
|
CONSTRAINT
|
|
/\ Len(firstName) <= 10
|
|
/\ Len(lastName) <= 10
|
|
/\ Len(productName) <= 15
|
|
/\ Len(email) <= 20
|