I am learning PVS by modeling unlabeled and labeled transition systems (TS) in PVS. Unlabeled transition system consists of a set of states, an initial state and a set of transitions from one state to another. Labeled transitin system has an extra set of events (labels). Specification is as follows:
TS[state, event: TYPE]: THEORY BEGIN
states:TYPE = [#loc: state#] %i have defined states as record structure as it will be easy to add a field for time in the future.
transition: TYPE = [# source: state, dest: state #]
pre_UTS: TYPE = [# States: setof[states], s0: state,
Transitions: setof[transition] #]
pre_LTS: TYPE = [# States: setof[states], s0: state,
Event: setof[event], Transitions: setof[transition] #]
UTS: VAR pre_UTS
LTS: VAR pre_LTS
Is above specification is right? or do i need to add something more?
Your kind suggestions are welcomed.