STATIC SEMI-ORDER CONVERSION

摘要

PROBLEM TO BE SOLVED: To attain the use of an existing model checking tool with no correction required by producing a state graph generator having a corrected multiprocessing system to be checked by adding many rules to a generator to much reduce the state graph to be generated. SOLUTION: The initial state of a system is selected based on a certain initial condition (100) and stored in a list. Then all enable subsequent states are calculated from the selected initial state and a subset of enable transistors coincident with conditions C0 and C1 is selected about an ample set (110). If the subset is not detected (120), an entire set of enable transitions is selected (130). Then a state where every transition contained in the ample set moves in the system is calculated (140) and stored in the list (150). Then it's judged whether a state that is not studied yet is displayed (160). If the said state is displayed, a transition that is not studied yet is selected from the list (170).