diff --git a/demo/vehicle/controller/inc-expr-fsw4.py b/demo/vehicle/controller/inc-expr-fsw4.py
index 647a54fd1104f508e5c3e6132b5798abcdb61f45..f008a0b0c18f07f8fd09f6ecaa227db8c34f0ed4 100644
--- a/demo/vehicle/controller/inc-expr-fsw4.py
+++ b/demo/vehicle/controller/inc-expr-fsw4.py
@@ -9,86 +9,79 @@ class LaneObjectMode(Enum):
Signal = auto() # Traffic lights
Obstacle = auto() # Static (to road/lane) obstacles
-class VehicleMode(Enum):
+class AgentMode(Enum):
Normal = auto()
SwitchLeft = auto()
SwitchRight = auto()
Brake = auto()
Stop = auto()
-class LaneMode(Enum):
- Lane0 = auto()
- Lane1 = auto()
- Lane2 = auto()
+class TrackMode(Enum):
+ T0 = auto()
+ T1 = auto()
+ T2 = auto()
+ T3 = auto()
+ T4 = auto()
+ M40 = auto()
+ M01 = auto()
+ M12 = auto()
+ M23 = auto()
+ M04 = auto()
+ M10 = auto()
+ M21 = auto()
+ M32 = auto()
class State:
x = 0.0
y = 0.0
theta = 0.0
v = 0.0
- vehicle_mode: VehicleMode = VehicleMode.Normal
- lane_mode: LaneMode = LaneMode.Lane0
+ agent_mode: AgentMode = AgentMode.Normal
+ track_mode: TrackMode = TrackMode.T0
type: LaneObjectMode = LaneObjectMode.Vehicle
- def __init__(self, x, y, theta, v, vehicle_mode: VehicleMode, lane_mode: LaneMode, type: LaneObjectMode):
- pass
-
def car_front(ego, others, lane_map, thresh_far, thresh_close):
- return any((lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) > thresh_close \
- and lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) < thresh_far \
- and ego.lane_mode == other.lane_mode) for other in others)
+ return any((lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) > thresh_close \
+ and lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) < thresh_far \
+ and ego.track_mode == other.track_mode) for other in others)
def car_left(ego, others, lane_map):
- return any((lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) < 8 and \
- lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) >-3 and \
- other.lane_mode==lane_map.left_lane(ego.lane_mode)) for other in others)
+ return any((lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) < 8 and \
+ lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) >-3 and \
+ other.track_mode==lane_map.left_lane(ego.track_mode)) for other in others)
def car_right(ego, others, lane_map):
- return any((lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) < 8 and \
- lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) >-3 and \
- other.lane_mode==lane_map.right_lane(ego.lane_mode)) for other in others)
+ return any((lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) < 8 and \
+ lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) >-3 and \
+ other.track_mode==lane_map.right_lane(ego.track_mode)) for other in others)
def controller(ego:State, others:List[State], lane_map):
output = copy.deepcopy(ego)
- if ego.vehicle_mode == VehicleMode.Normal:
- # Switch left if left lane is empty
- if car_front(ego, others, lane_map, 4.5, 3):
- if lane_map.has_left(ego.lane_mode) and \
+ if ego.agent_mode == AgentMode.Normal:
+ if car_front(ego, others, lane_map, 4, 3):
+ # Switch left if left lane is empty
+ if lane_map.h_exist(ego.track_mode, ego.agent_mode, AgentMode.SwitchLeft) and \
not car_left(ego, others, lane_map):
- output.vehicle_mode = VehicleMode.SwitchLeft
-
- # Switch right if right lane is empty
- if car_front(ego, others, lane_map, 4.5, 3):
- if lane_map.has_right(ego.lane_mode) and \
+ output.agent_mode = AgentMode.SwitchLeft
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.SwitchLeft)
+
+ # Switch right if right lane is empty
+ if lane_map.h_exist(ego.track_mode, ego.agent_mode, AgentMode.SwitchRight) and \
not car_right(ego, others, lane_map):
- output.vehicle_mode = VehicleMode.SwitchRight
-
- # # If really close just brake
- # if car_front(ego, others, lane_map, 2, -0.5):
- # output.vehicle_mode = VehicleMode.Stop
- # output.v = 0.1
+ output.agent_mode = AgentMode.SwitchRight
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.SwitchRight)
# If switched left enough, return to normal mode
- if ego.vehicle_mode == VehicleMode.SwitchLeft:
- if lane_map.get_lateral_distance(ego.lane_mode, [ego.x, ego.y]) >= (lane_map.get_lane_width(ego.lane_mode)-0.2):
- output.vehicle_mode = VehicleMode.Normal
- output.lane_mode = lane_map.left_lane(ego.lane_mode)
+ if ego.agent_mode == AgentMode.SwitchLeft:
+ if lane_map.get_lateral_distance(ego.track_mode, [ego.x, ego.y]) >= (lane_map.get_lane_width(ego.track_mode)-0.2):
+ output.agent_mode = AgentMode.Normal
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.Normal)
# If switched right enough,return to normal mode
- if ego.vehicle_mode == VehicleMode.SwitchRight:
- if lane_map.get_lateral_distance(ego.lane_mode, [ego.x, ego.y]) <= -(lane_map.get_lane_width(ego.lane_mode)-0.2):
- output.vehicle_mode = VehicleMode.Normal
- output.lane_mode = lane_map.right_lane(ego.lane_mode)
-
- # if ego.vehicle_mode == VehicleMode.Brake:
- # if all((\
- # (lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) -\
- # lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) > 5 or \
- # lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) -\
- # lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) < -0.5) and\
- # other.lane_mode==ego.lane_mode) for other in others):
- # output.vehicle_mode = VehicleMode.Normal
- # output.v = 1.0
+ if ego.agent_mode == AgentMode.SwitchRight:
+ if lane_map.get_lateral_distance(ego.track_mode, [ego.x, ego.y]) <= -(lane_map.get_lane_width(ego.track_mode)-0.2):
+ output.agent_mode = AgentMode.Normal
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.Normal)
return output
diff --git a/demo/vehicle/controller/inc-expr-fsw7.py b/demo/vehicle/controller/inc-expr-fsw7.py
index 5c6b00a196b2d90592f133a8bec362d7c81e861e..ed5e4b4957035fc8a957014108a4a589ce46d8e4 100644
--- a/demo/vehicle/controller/inc-expr-fsw7.py
+++ b/demo/vehicle/controller/inc-expr-fsw7.py
@@ -9,70 +9,79 @@ class LaneObjectMode(Enum):
Signal = auto() # Traffic lights
Obstacle = auto() # Static (to road/lane) obstacles
-class VehicleMode(Enum):
+class AgentMode(Enum):
Normal = auto()
SwitchLeft = auto()
SwitchRight = auto()
Brake = auto()
Stop = auto()
-class LaneMode(Enum):
- Lane0 = auto()
- Lane1 = auto()
- Lane2 = auto()
+class TrackMode(Enum):
+ T0 = auto()
+ T1 = auto()
+ T2 = auto()
+ T3 = auto()
+ T4 = auto()
+ M40 = auto()
+ M01 = auto()
+ M12 = auto()
+ M23 = auto()
+ M04 = auto()
+ M10 = auto()
+ M21 = auto()
+ M32 = auto()
class State:
x = 0.0
y = 0.0
theta = 0.0
v = 0.0
- vehicle_mode: VehicleMode = VehicleMode.Normal
- lane_mode: LaneMode = LaneMode.Lane0
+ agent_mode: AgentMode = AgentMode.Normal
+ track_mode: TrackMode = TrackMode.T0
type: LaneObjectMode = LaneObjectMode.Vehicle
- def __init__(self, x, y, theta, v, vehicle_mode: VehicleMode, lane_mode: LaneMode, type: LaneObjectMode):
- pass
-
def car_front(ego, others, lane_map, thresh_far, thresh_close):
- return any((lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) > thresh_close \
- and lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) < thresh_far \
- and ego.lane_mode == other.lane_mode) for other in others)
+ return any((lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) > thresh_close \
+ and lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) < thresh_far \
+ and ego.track_mode == other.track_mode) for other in others)
def car_left(ego, others, lane_map):
- return any((lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) < 8 and \
- lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) >-3 and \
- other.lane_mode==lane_map.left_lane(ego.lane_mode)) for other in others)
+ return any((lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) < 8 and \
+ lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) >-3 and \
+ other.track_mode==lane_map.left_lane(ego.track_mode)) for other in others)
def car_right(ego, others, lane_map):
- return any((lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) < 8 and \
- lane_map.get_longitudinal_position(other.lane_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.lane_mode, [ego.x,ego.y]) >-3 and \
- other.lane_mode==lane_map.right_lane(ego.lane_mode)) for other in others)
+ return any((lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) < 8 and \
+ lane_map.get_longitudinal_position(other.track_mode, [other.x,other.y]) - lane_map.get_longitudinal_position(ego.track_mode, [ego.x,ego.y]) >-3 and \
+ other.track_mode==lane_map.right_lane(ego.track_mode)) for other in others)
def controller(ego:State, others:List[State], lane_map):
output = copy.deepcopy(ego)
- if ego.vehicle_mode == VehicleMode.Normal:
+ if ego.agent_mode == AgentMode.Normal:
if car_front(ego, others, lane_map, 7, 3):
# Switch left if left lane is empty
- if lane_map.has_left(ego.lane_mode) and \
+ if lane_map.h_exist(ego.track_mode, ego.agent_mode, AgentMode.SwitchLeft) and \
not car_left(ego, others, lane_map):
- output.vehicle_mode = VehicleMode.SwitchLeft
-
+ output.agent_mode = AgentMode.SwitchLeft
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.SwitchLeft)
+
# Switch right if right lane is empty
- if lane_map.has_right(ego.lane_mode) and \
+ if lane_map.h_exist(ego.track_mode, ego.agent_mode, AgentMode.SwitchRight) and \
not car_right(ego, others, lane_map):
- output.vehicle_mode = VehicleMode.SwitchRight
-
+ output.agent_mode = AgentMode.SwitchRight
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.SwitchRight)
+
# If switched left enough, return to normal mode
- if ego.vehicle_mode == VehicleMode.SwitchLeft:
- if lane_map.get_lateral_distance(ego.lane_mode, [ego.x, ego.y]) >= (lane_map.get_lane_width(ego.lane_mode)-0.2):
- output.vehicle_mode = VehicleMode.Normal
- output.lane_mode = lane_map.left_lane(ego.lane_mode)
+ if ego.agent_mode == AgentMode.SwitchLeft:
+ if lane_map.get_lateral_distance(ego.track_mode, [ego.x, ego.y]) >= (lane_map.get_lane_width(ego.track_mode)-0.2):
+ output.agent_mode = AgentMode.Normal
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.Normal)
# If switched right enough,return to normal mode
- if ego.vehicle_mode == VehicleMode.SwitchRight:
- if lane_map.get_lateral_distance(ego.lane_mode, [ego.x, ego.y]) <= -(lane_map.get_lane_width(ego.lane_mode)-0.2):
- output.vehicle_mode = VehicleMode.Normal
- output.lane_mode = lane_map.right_lane(ego.lane_mode)
+ if ego.agent_mode == AgentMode.SwitchRight:
+ if lane_map.get_lateral_distance(ego.track_mode, [ego.x, ego.y]) <= -(lane_map.get_lane_width(ego.track_mode)-0.2):
+ output.agent_mode = AgentMode.Normal
+ output.track_mode = lane_map.h(ego.track_mode, ego.agent_mode, AgentMode.Normal)
return output
diff --git a/demo/vehicle/inc-expr.py b/demo/vehicle/inc-expr.py
index aae35fea6afd1aa526ecf49dd9d4f1875d6c3cf8..8a274ddcc6db25f81e36e0d9013a24844a8e8407 100644
--- a/demo/vehicle/inc-expr.py
+++ b/demo/vehicle/inc-expr.py
@@ -86,7 +86,7 @@ def run(sim, meas=False):
pp({
"dur": timeit.default_timer() - time,
"cache_size": cache_size,
- "node_count": len(traces.nodes),
+ "node_count": ((0 if sim else scenario.verifier.num_transitions), len(traces.nodes)),
"hits": scenario.simulator.cache_hits if sim else (scenario.verifier.tube_cache_hits, scenario.verifier.trans_cache_hits),
})
diff --git a/inc-expr.py b/inc-expr.py
index 3e94f1a22961b133214daa20a7f583cf773cd4c8..2f1fbffa5002ef3d5eceea6f3437a42a975a000b 100644
--- a/inc-expr.py
+++ b/inc-expr.py
@@ -11,7 +11,7 @@ class ExperimentResult:
max_mem: float
duration: float
cache_size: float
- node_count: int
+ node_count: Tuple[int, int]
ret_code: int
cache_hits: Union[Tuple[int, int], Tuple[Tuple[int, int], Tuple[int, int]]]
@@ -53,4 +53,4 @@ for i in range(0, len(rslts), 2):
name = "change ctlr"
cache_hit_rate = inc.cache_hits[0] / (inc.cache_hits[0] + inc.cache_hits[1]) if "v" not in var else (inc.cache_hits[0][0] + inc.cache_hits[1][0]) / (inc.cache_hits[0][0] + inc.cache_hits[0][1] + inc.cache_hits[1][0] + inc.cache_hits[1][1])
- print(" & " + " & ".join([name] + [str(i) for i in [inc.node_count, round(no.duration, 2), round(no.max_mem), round(inc.duration, 2), round(inc.max_mem), round(inc.cache_size, 2), round(cache_hit_rate * 100, 2)]]) + " \\\\")
+ print(" & " + " & ".join([name] + [str(i) for i in [inc.node_count[1], round(no.duration, 2), round(no.max_mem), round(inc.duration, 2), round(inc.max_mem), round(inc.cache_size, 2), round(cache_hit_rate * 100, 2)]]) + " \\\\")