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),Clock('C4',0,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,0,0,0),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,0,0,0),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,0,0,0)]))
+net.add_place(Place("terminal",[Terminal([0,0,0],[0,0,0],[False,False,False],[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)) and (C4<MaxCom_C4 or (C4DidBroadcast and C4<S_C4))')"))
+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("decisionTer", "c.id=='C4'and c.v>=S_C4 and t.id=='C0' and t.v<S_C0 and d.id=='C1' and d.v<S_C1"))
+net.add_input("clocks", "decisionTer", MultiArc(Variable("c"),Test(Variable("t")),Test(Variable("d"))))
+net.add_input("vehicles", "decisionTer", Flush("vehicles"))
+net.add_input("terminal", "decisionTer", Variable("ter"))
+net.add_output("clocks", "decisionTer", Expression("c.reset()"))
+net.add_output("vehicles", "decisionTer", Fill("vehicles"))
+net.add_output("terminal", "decisionTer", Expression("ter.compute(vehicles)"))
+
+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_input("terminal", "broadcastV1", Variable("ter"))
+net.add_output("clocks", "broadcastV1", Expression("c.statuschange()"))
+net.add_output("vehicles", "broadcastV1", Fill("Vehicle.broadcast(vehicles,0)"))
+net.add_output("terminal", "broadcastV1", Expression("ter.receive_data(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_input("terminal", "broadcastV2", Variable("ter"))
+net.add_output("clocks", "broadcastV2", Expression("c.statuschange()"))
+net.add_output("vehicles", "broadcastV2", Fill("Vehicle.broadcast(vehicles,1)"))
+net.add_output("terminal", "broadcastV2", Expression("ter.receive_data(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_input("terminal", "broadcastV3", Variable("ter"))
+net.add_output("clocks", "broadcastV3", Expression("c.statuschange()"))
+net.add_output("vehicles", "broadcastV3", Fill("Vehicle.broadcast(vehicles,2)"))
+net.add_output("terminal", "broadcastV3", Expression("ter.receive_data(vehicles,2)"))
+
+net.add_transition(Transition("broadcastTer", "c.id=='C4'and c.v>=MinCom_C4 and not c.b and t.id=='C0' and t.v<S_C0"))
+net.add_input("clocks", "broadcastTer", MultiArc(Variable("c"),Test(Variable("t"))))
+net.add_input("vehicles", "broadcastTer", Flush("vehicles"))
+net.add_input("terminal", "broadcastTer", Variable("ter"))
+net.add_output("clocks", "broadcastTer", Expression("c.statuschange()"))
+net.add_output("vehicles", "broadcastTer", Fill("Vehicle.give_orders(vehicles,ter)"))
+net.add_output("terminal", "broadcastTer", Expression("ter"))
+
+net.build(saveto="netverifcar.py")