[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Help regarding Transition System modeling in PVS
There are many ways to specify transition systems and they are bad or god
depending on what you want to do with it. For example, if you are
planning to animate the specification using PVSio, I would probably use
some ³computational types² such as lists instead of sets. However, if your
plan is to reason about them, sets are probably a better option.
Regarding your TS theory, it looks good so far. I only have two comments.
If you are not sure what structure you need for states, you could avoid
the definition of the type ³states² and use the parametric type ³state²
instead. Later one, when you need a more precise definition, you could
import this theory and instantiate the type ³state" accordingly. Also,
notice that the field ³States² in pre_UTS and pre_LTS is not doing much in
those definitions. For example, if your intention is that s0 is in that
set or that your transitions are only defined for elements of that set,
your specification is not accomplishing that. A ³simpler² way to
accomplish this is to define a parametric variable States : setof[state],
TS[state, event: TYPE, States:setof[state]]: THEORY BEGIN
transition: TYPE = [# source: (States), dest: (States) #]
pre_UTS: TYPE = [# s0: (States), Transitions: setof[transition] #]
Hope that this helps,
Cesar A. Munoz, NASA <Cesar.A.Munoz@xxxxxxxx>
NASA Langley Research Center, Bldg. 1220, Room 115 MS. 130, Hampton, VA
Office: +1 (757) 864 1446. Fax: +1 (757) 864 4234
From: <pvs-help-bounces+cesar.a.munoz=nasa.gov@xxxxxxxxxxx> on behalf of
Saqib Nawaz <saqib_dola@xxxxxxxxx>
Reply-To: Saqib Nawaz <saqib_dola@xxxxxxxxx>
Date: Thursday, November 24, 2016 at 12:44 AM
To: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>
Subject: [PVS-Help] Help regarding Transition System modeling in PVS
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.