[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Help regarding Transition System modeling in PVS



Hi all,

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 #]

%unlabled TS
pre_UTS: TYPE = [# States: setof[states], s0: state,
                 Transitions: setof[transition] #]
%labeled TS
pre_LTS: TYPE = [# States: setof[states], s0: state,
                Event: setof[event], Transitions: setof[transition] #]

UTS: VAR pre_UTS
LTS: VAR pre_LTS

END TS

Is above specification is right? or do i need to add something more?
Your kind suggestions are welcomed.

Regards,
Saqib