Commit da99b1ff authored by Jae Young Lee's avatar Jae Young Lee

Change LTL_test (independent module)

parent 2cedd22c
from . import LTLProperty
from env.simple_intersection import APdict
from model_checker.simple_intersection import LTLProperty
from model_checker.simple_intersection.AP_dict import AP_dict_simple_intersection
from model_checker import Parser
# TODO: Refactor LTL_test to model_checker part.
def test_model_check(trace):
def test_model_check(LTL, trace):
print(trace)
for i in range(0, len(trace)):
LTL.check_incremental(trace[i])
print("incremental result:" + str(LTL.result))
......@@ -13,18 +15,36 @@ def test_model_check(trace):
print("batch result:" + str(LTL.result) + "\n")
print("True: " + str(Parser.TRUE))
print("Undecided: " + str(Parser.UNDECIDED))
print("False: " + str(Parser.FALSE))
LTL = LTLProperty("G (has_entered_stop_region => (in_stop_region U has_stopped_in_stop_region) )", -100)
trace = [0, 0, 0, 0, 0, 0, 0,
0 | int(pow(2, AP_dict['has_entered_stop_region'])) | int(pow(2, AP_dict['in_stop_region']))
]
print(trace)
test_model_check(trace)
0 | int(pow(2, AP_dict_simple_intersection['has_entered_stop_region'])) | int(pow(2, AP_dict_simple_intersection['in_stop_region']))]
test_model_check(LTL, trace)
trace = [0, 0, 0, 0, 0, 0, 0,
0 | int(pow(2, AP_dict['has_entered_stop_region'])) | int(pow(2, AP_dict['in_stop_region'])),
0 | int(pow(2, AP_dict['has_entered_stop_region']))
]
print(trace)
test_model_check(trace)
0 | int(pow(2, AP_dict_simple_intersection['has_entered_stop_region'])) | int(pow(2, AP_dict_simple_intersection['in_stop_region'])),
0 | int(pow(2, AP_dict_simple_intersection['has_entered_stop_region']))]
test_model_check(LTL, trace)
PL = LTLProperty("in_stop_region and stopped_now", -100)
trace = [0 | int(pow(2, AP_dict_simple_intersection['stopped_now'])) | int(pow(2, AP_dict_simple_intersection['in_stop_region'])),
0, 0, 0, 0, 0, 0]
test_model_check(PL, trace)
trace = [0 | 0 | int(pow(2, AP_dict_simple_intersection['in_stop_region'])),
0, 0, 0, 0, 0, 0]
test_model_check(PL, trace)
trace = [0 | int(pow(2, AP_dict_simple_intersection['stopped_now'])) | 0,
0, 0, 0, 0, 0, 0]
test_model_check(PL, trace)
trace = [0, 0, 0, 0, 0, 0, 0]
test_model_check(PL, trace)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment