vdm-sl 中的智能停车模型
类型
Id = token;
Status = <EMPTY> | <OCCUPIED>;
Type = <A> | <B> | <C> | <D> | <E>;
Node :: id : Id
status : Status
indegree : nat
outdegree : nat
type : Type
dist : int
inv mk_Node(-,-,indegree,outdegree,type,-)
== type = <A> => indegree = 2
and outdegree = 2 and
type = <B> => indegree = 1
and outdegree = 2 and
type = <C> => indegree = 1
and outdegree = 1 and
type = <D> => indegree = 3
and outdegree = 3 and
type = <E> => indegree = 2
and outdegree = 1;
Direction = <UNDIRECTED> | <DIRECTED>;
Edge :: end1 : Node
end2 : Node
direction : Direction;
Passage :: pnodes : set of Node
pedges : set of Edge inv
mk_Passage(pnodes, pedges)==
forall pn in set pnodes &
pn.type = <A> or
pn.type = <B> or
pn.type = <C> or
pn.type = <E> and
forall pe in set pedges &
pe.direction = <DIRECTED>;
PKArea = <LEFT> | <RIGHT>;
Parking :: pknodes : set of Node
pkedges : set of Edge
pkarea : PKArea
inv mk_Parking(pknodes, pkedges, pkarea)==
exists pkn1 in set pknodes & pkn1.type = <D> => pkarea = <LEFT>
or pkarea = <RIGHT> and
exists pke1, pke2 in set pkedges &
pke1.direction = <UNDIRECTED> and
pke2.direction = <UNDIRECTED> and
exists pke3, pke4 in set pkedges &
pke3.direction = <DIRECTED> and
pke4.direction = <DIRECTED> and
exists pkn2 in set pknodes &
pkn2.type = <C> and exists
pke5 in set pkedges &
pke5.direction = <UNDIRECTED>;
Credit = nat;
Car :: id : Id
ccard : Credit;
Entrance = <RCAR_CAENTRANCE> | <RCAR_CAEXIT>;
Exit = <RCAR_CAENTRANCE> | <RCAR_CAEXIT>;
Sense :: entrance : Entrance
sexit : Exit;
Sensor :: id : Id
car : Car
sense : Sense
inv mk_Sensor(-, car, sense)== HaveCredit(car) and
sense.entrance = <RCAR_CAENTRANCE> and
sense.entrance = <RCAR_CAEXIT> and
sense.sexit = <RCAR_CAENTRANCE> and
sense.sexit = <RCAR_CAEXIT>;
功能
HaveCredit(car : Car) hc : bool
pre true
post hc <=> (car.ccard >= 30);
错误行操作 = ; Actor :: id : Id action : 动作 inv mk_Actor(-, action)== action = ;
Barrier = token;
Controller :: cid : Id
rcars : set of Car;
Topology :: passages : set of Passage
parkings : set of Parking
gent : Node
gexit : Node
barriers : set of Barrier
sensors : set of Sensor
actors : set of Actor
controller : Controller;
state SParkingSystem of
topology : [Topology]
init pks == pks =
mk_SParkingSystem(nil) end
操作
AllowToEnter()
ext wr topology :
[Topology] pre true
post exists ps in set topology.sensors &
forall rc in set topology.controller.rcars
&
ps.sense.entrance = <RCAR_CAENTRANCE>
and HaveCredit(rc) =>
exists ac in set topology.actors &
ac.action = <OPEN_BARRIER> and
ps.sense.entrance = <RCAR_CAEXIT>;
SearchPAreas()ext rd topology :[Topology]
pre true
post forall pk in set topology.parkings
& forall pkn in set pk.pknodes &
pkn.type = <C> and
pkn.status = <EMPTY> ;
DisplayPAreas()sorted : seq of Node, nearest
: Node
ext rd topology : [Topology] pre true
post forall sqpk : seq of Parking &
forall i in set inds sqpk &
sqpk(i).pkarea = <RIGHT> and
sqpk(i).pkarea = <LEFT> and
forall sqn : seq of Node & elems sqn
= sqpk(i).pknodes and forall pkn1,
pkn2 in set elems sqn & pkn1.status
= <EMPTY> and pkn2.status =
<EMPTY> and forall i in set inds
sqn &
i < i+1 => sqn(i) = pkn1 and
sqn(i+1) = pkn2 and
sqn(i).type = <C> and
sqn(i).status = <EMPTY> and
sqn(i+1).type = <C> and
sqn(i+1).status = <EMPTY> and
sorted = sqn and
sqn(i).dist < sqn(i+1).dist
=> nearest = sqn(i);
AllowToExit()
ext wr topology :
[Topology] pre true
post exists ps in set topology.sensors &
forall rc in set topology.controller.rcars &
ps.sense.sexit = <RCAR_CAENTRANCE> and
forall t : Time &
DeductCredit(t, rc.ccard) or
not DeductCredit(t, rc.ccard) and
forall c : Credit &
Recharge(c) and
DeductCredit(t, rc.ccard) and
exists ac in set topology.actors &
ac.action = <OPEN_BARRIER> and
ps.sense.sexit = <RCAR_CAEXIT>;
错误行：
DeductCredit(t : Time, credit : Credit) dc :
bool
ext wr topology : [Topology]
pre true
post dc <=>
forall rc in set topology.controller.rcars
& credit = rc.ccard and
t.hour = 1 => rc.ccard = credit - 30;
Recharge (credit : Credit) rc : bool
ext wr topology :
[Topology] pre true
post rc <=> forall rc in set
topology.controller.rcars &
rc.ccard = rc.ccard + credit;