i have two errors in vdm sl project , 1) Action = <OPEN_BARRIER>; 2) Time :: hour : nat;

Question

smart parking model in vdm-sl

types

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

functions

HaveCredit(car : Car) hc : bool 
pre true 
post hc <=> (car.ccard  >= 30);

ERROR Line Action = ; Actor :: id : Id action : 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 

operations

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

ERROR Line:

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;

Answer 1

It's difficult to make out on the screen image, but it looks like you've mixed the type definition for Time with the function definitions for DeductCredit etc. You need to put types, functions (and operations, values etc) in their own section, introduced with "types" or "functions" etc. Though note that you can have repeated "types" sections, if you want to locate a type definition close to the functions that use it.