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’]] = False

APs[‘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}

Module contents