Toggle navigation
Toggle navigation
This project
Loading...
Sign in
Johan ARCILE
/
MAPTs
Go to a project
Toggle navigation
Toggle navigation pinning
Projects
Groups
Snippets
Help
Project
Activity
Repository
Pipelines
Graphs
Issues
0
Merge Requests
0
Wiki
Network
Create a new issue
Builds
Commits
Authored by
Johan ARCILE
2019-11-12 13:48:10 +0000
Browse Files
Options
Browse Files
Download
Email Patches
Plain Diff
Commit
2292d79b529f443d263169a7254228da7f068416
2292d79b
1 parent
4d2add28
Upload new file
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
57 additions
and
0 deletions
Models/Model3/verifcar.py
Models/Model3/verifcar.py
0 → 100644
View file @
2292d79
from
zinc.nets
import
*
from
libsverifcar
import
*
net
=
PetriNet
(
"VerifCar"
)
net
.
declare
(
"from libsverifcar import *"
)
for
k
,
v
in
constants
.
items
()
:
net
.
declare
(
"
%
s =
%
r"
%
(
k
,
v
))
net
.
add_place
(
Place
(
"clocks"
,[
Clock
(
'C0'
,
0
,
True
),
Clock
(
'C1'
,
0
,
True
),
Clock
(
'C2'
,
3
,
True
),
Clock
(
'C3'
,
7
,
True
)]))
net
.
add_place
(
Place
(
"vehicles"
,[
Vehicle
(
0
,
True
,(
0
*
scale
)
//
GranX
,(
525
*
scale
)
//
GranY
,(
3000
*
scale
)
//
GranV
,(
3
*
scale
)
//
GranA
,
0
,
navigation_list
[
0
],[
0
,
0
,
0
],[
0
,
0
,
0
],
0
,[
False
,
False
,
False
],[
False
,
False
,
False
]),
Vehicle
(
1
,
True
,(
3000
*
scale
)
//
GranX
,(
875
*
scale
)
//
GranY
,(
1500
*
scale
)
//
GranV
,(
3
*
scale
)
//
GranA
,
0
,
navigation_list
[
1
],[
0
,
0
,
0
],[
0
,
0
,
0
],
0
,[
False
,
False
,
False
],[
False
,
False
,
False
]),
Vehicle
(
2
,
True
,(
4000
*
scale
)
//
GranX
,(
175
*
scale
)
//
GranY
,(
2000
*
scale
)
//
GranV
,(
3
*
scale
)
//
GranA
,
0
,
navigation_list
[
2
],[
0
,
0
,
0
],[
0
,
0
,
0
],
0
,[
False
,
False
,
False
],[
False
,
False
,
False
])]))
net
.
add_transition
(
Transition
(
"tic"
,
"Clock.check(clocks,'C0<S_C0 and (C1<MaxCom_C1 or (C1DidBroadcast and C1<S_C1)) and (C2<MaxCom_C2 or (C2DidBroadcast and C2<S_C2)) and (C3<MaxCom_C3 or (C3DidBroadcast and C3<S_C3))')"
))
net
.
add_input
(
"clocks"
,
"tic"
,
Flush
(
"clocks"
))
net
.
add_output
(
"clocks"
,
"tic"
,
Fill
(
"Clock.update(clocks)"
))
net
.
add_transition
(
Transition
(
"update"
,
"c.id=='C0' and c.v>=S_C0"
))
net
.
add_input
(
"clocks"
,
"update"
,
Variable
(
"c"
))
net
.
add_input
(
"vehicles"
,
"update"
,
Flush
(
"vehicles"
))
net
.
add_output
(
"clocks"
,
"update"
,
Expression
(
"c.reset()"
))
net
.
add_output
(
"vehicles"
,
"update"
,
Fill
(
"Vehicle.update(vehicles)"
))
net
.
add_transition
(
Transition
(
"decisionV1"
,
"c.id=='C1'and c.v>=S_C1 and t.id=='C0' and t.v<S_C0"
))
net
.
add_input
(
"clocks"
,
"decisionV1"
,
MultiArc
(
Variable
(
"c"
),
Test
(
Variable
(
"t"
))))
net
.
add_input
(
"vehicles"
,
"decisionV1"
,
Flush
(
"vehicles"
))
net
.
add_output
(
"clocks"
,
"decisionV1"
,
Expression
(
"c.reset()"
))
net
.
add_output
(
"vehicles"
,
"decisionV1"
,
Fill
(
"Vehicle.decision(vehicles,0)"
))
net
.
add_transition
(
Transition
(
"decisionV2"
,
"c.id=='C2'and c.v>=S_C2 and t.id=='C0' and t.v<S_C0"
))
net
.
add_input
(
"clocks"
,
"decisionV2"
,
MultiArc
(
Variable
(
"c"
),
Test
(
Variable
(
"t"
))))
net
.
add_input
(
"vehicles"
,
"decisionV2"
,
Flush
(
"vehicles"
))
net
.
add_output
(
"clocks"
,
"decisionV2"
,
Expression
(
"c.reset()"
))
net
.
add_output
(
"vehicles"
,
"decisionV2"
,
Fill
(
"Vehicle.decision(vehicles,1)"
))
net
.
add_transition
(
Transition
(
"decisionV3"
,
"c.id=='C3'and c.v>=S_C3 and t.id=='C0' and t.v<S_C0"
))
net
.
add_input
(
"clocks"
,
"decisionV3"
,
MultiArc
(
Variable
(
"c"
),
Test
(
Variable
(
"t"
))))
net
.
add_input
(
"vehicles"
,
"decisionV3"
,
Flush
(
"vehicles"
))
net
.
add_output
(
"clocks"
,
"decisionV3"
,
Expression
(
"c.reset()"
))
net
.
add_output
(
"vehicles"
,
"decisionV3"
,
Fill
(
"Vehicle.decision(vehicles,2)"
))
net
.
add_transition
(
Transition
(
"broadcastV1"
,
"c.id=='C1'and c.v>=MinCom_C1 and not c.b and t.id=='C0' and t.v<S_C0"
))
net
.
add_input
(
"clocks"
,
"broadcastV1"
,
MultiArc
(
Variable
(
"c"
),
Test
(
Variable
(
"t"
))))
net
.
add_input
(
"vehicles"
,
"broadcastV1"
,
Flush
(
"vehicles"
))
net
.
add_output
(
"clocks"
,
"broadcastV1"
,
Expression
(
"c.statuschange()"
))
net
.
add_output
(
"vehicles"
,
"broadcastV1"
,
Fill
(
"Vehicle.broadcast(vehicles,0)"
))
net
.
add_transition
(
Transition
(
"broadcastV2"
,
"c.id=='C2'and c.v>=MinCom_C2 and not c.b and t.id=='C0' and t.v<S_C0"
))
net
.
add_input
(
"clocks"
,
"broadcastV2"
,
MultiArc
(
Variable
(
"c"
),
Test
(
Variable
(
"t"
))))
net
.
add_input
(
"vehicles"
,
"broadcastV2"
,
Flush
(
"vehicles"
))
net
.
add_output
(
"clocks"
,
"broadcastV2"
,
Expression
(
"c.statuschange()"
))
net
.
add_output
(
"vehicles"
,
"broadcastV2"
,
Fill
(
"Vehicle.broadcast(vehicles,1)"
))
net
.
add_transition
(
Transition
(
"broadcastV3"
,
"c.id=='C3'and c.v>=MinCom_C3 and not c.b and t.id=='C0' and t.v<S_C0"
))
net
.
add_input
(
"clocks"
,
"broadcastV3"
,
MultiArc
(
Variable
(
"c"
),
Test
(
Variable
(
"t"
))))
net
.
add_input
(
"vehicles"
,
"broadcastV3"
,
Flush
(
"vehicles"
))
net
.
add_output
(
"clocks"
,
"broadcastV3"
,
Expression
(
"c.statuschange()"
))
net
.
add_output
(
"vehicles"
,
"broadcastV3"
,
Fill
(
"Vehicle.broadcast(vehicles,2)"
))
net
.
build
(
saveto
=
"netverifcar.py"
)
Please
register
or
login
to post a comment