时间戳

首页 > 解决方案 > 我在 vdm sl 项目中有两个错误，1) 操作 =; 2）时间：：小时：nat；

eclipse - 我在 vdm sl 项目中有两个错误，1) 操作 =; 2）时间：：小时：nat；

问题描述

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>;

错误行：

时间 :: 小时 : nat;

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;

标签： eclipsedslmodelingvdm++vdm-sl

解决方案

在屏幕图像上很难辨认，但看起来您已经将 Time 的类型定义与 DeductCredit 等的函数定义混合在一起。您需要将类型、函数（和操作、值等）放在它们自己的部分中，与“类型”或“函数”等一起引入。尽管请注意，如果您想找到靠近使用它的函数的类型定义，则可以有重复的“类型”部分。

推荐阅读