verifier.simple_intersection package¶
Submodules¶
verifier.simple_intersection.AP_dict module¶
verifier.simple_intersection.LTL_test module¶
-
verifier.simple_intersection.LTL_test.
test_model_check
(LTL, trace)¶
verifier.simple_intersection.classes module¶
-
class
verifier.simple_intersection.classes.
AtomicPropositions
¶ Bases:
verifier.atomic_propositions_base.AtomicPropositionsBase
An AP-control class for AP-wise manipulation as shown in the example:
APs = AtomicPropositions() APs[0] = False # this is same as
# APs[AP_dict[‘stop_region’]] = FalseAPs[‘in_stop_region’] = False # both expressions are the same
- Requires:
- Index in […] is an integer should be in the range {0,1,2, …, AP_dict_len}.
-
APdict
= {'before_but_close_to_stop_region': 2, 'before_intersection': 13, 'has_entered_stop_region': 1, 'has_stopped_in_stop_region': 4, 'highest_priority': 8, 'in_intersection': 5, 'in_stop_region': 0, 'intersection_is_clear': 9, 'lane': 11, 'on_route': 7, 'over_speed_limit': 6, 'parallel_to_lane': 12, 'stopped_now': 3, 'target_lane': 14, 'veh_ahead': 10, 'veh_ahead_stopped_now': 15, 'veh_ahead_too_close': 16}¶
-
class
verifier.simple_intersection.classes.
LTLProperty
(LTL_str, penalty, enabled=True)¶ Bases:
verifier.LTL_property_base.LTLPropertyBase
is a class that contains information of an LTL property in simple_intersection road scenario.
It encapsulates the model-checking part and contains additional information.
-
APdict
= {'before_but_close_to_stop_region': 2, 'before_intersection': 13, 'has_entered_stop_region': 1, 'has_stopped_in_stop_region': 4, 'highest_priority': 8, 'in_intersection': 5, 'in_stop_region': 0, 'intersection_is_clear': 9, 'lane': 11, 'on_route': 7, 'over_speed_limit': 6, 'parallel_to_lane': 12, 'stopped_now': 3, 'target_lane': 14, 'veh_ahead': 10, 'veh_ahead_stopped_now': 15, 'veh_ahead_too_close': 16}¶
-