Upload new file

+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,(5000*scale)//GranX,(525*scale)//GranY,(2000*scale)//GranV,(3*scale)//GranA,0,navigation_list[0],[0,0,0],[0,0,0],0),Vehicle(1,True,(0*scale)//GranX,(525*scale)//GranY,(3500*scale)//GranV,(3*scale)//GranA,0,navigation_list[1],[0,0,0],[0,0,0],0),Vehicle(2,True,(2000*scale)//GranX,(175*scale)//GranY,(2820*scale)//GranV,(3*scale)//GranA,0,navigation_list[2],[0,0,0],[0,0,0],0)]))
+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")