PURPOSE:To certify whether its proposition can be satisfied or not by providing a proposition input means for inputting an expression divided into a controllable object and an uncontrollable object, a state transition diagram generating means, a transition diagram synthesizing means and display means. CONSTITUTION:When a PTS++ expression (expression which can describe a state of an object of each event by dividing it into a controllable object and an uncontrollable object) is inputted from a proposition input part 1, a standard converting part 2 converts its expression to a standard format. Subsequently, in an initial graph generating part 7 of a transition diagram generating part 7, its proposition is decomposed to every fundamental unit, and also, decomposed more minutely. Next, each fundamental unit is converted to a state transition diagram. In this case, those which can reach each other are collected to one by a strong connection component summarizing part 8. Next, an edge synthesizing part 11 synthesizes all the state transition diagrams, while taking a pair into consideration. In such a case, an eliminating part 14 eliminates a part of the edge, while taking a pair into consideration. Thereafter, this result is displayed by a result display device 16.
展开▼
