(57)【特許請求の範囲】
【請求項１】
入出力順序系列仕様を表すデータにおける条件分岐と処理に、イベント及びアクションを特定する情報を付し、分岐の無い一本のパスにアクション実行パス状態を特定する情報を付し、一つのアクション実行パス状態について一つのレコードを有し、各レコードはイベント、前イベント、アクション系列を有する情報である状態定義レコード表を生成する第１の生成手段と、
前記状態定義レコード表に基づいて、前記状態定義レコード表に含まれるアクション実行パス状態ごとに一つのレコードを有し、各レコードは、前記状態定義レコード表に含まれる各イベントに対応するフィールドを有する情報である状態遷移表を生成する第２の生成手段と
を有する状態遷移表生成装置。
【請求項２】
入出力順序系列仕様を表すデータにおける条件分岐と処理に、イベント及びアクションを特定する情報を付し、条件分岐にアクション実行パス状態を特定する情報を付し、一つのアクション実行パス状態について一つ以上のレコードを有し、各レコードはイベント、前イベント、アクション系列を有する情報である状態定義レコード表を生成する第１の生成手段と、
前記状態定義レコード表に基づいて、前記状態定義レコード表に含まれるアクション実行パス状態ごとに一つのレコードを有し、各レコードは、前記状態定義レコード表に含まれる各イベントに対応するフィールドを有する情報である状態遷移表を生成する第２の生成手段と
を有する状態遷移表生成装置。
【請求項３】
前記第２の生成手段は、前記状態定義レコード表の処理対象レコードにおける前イベントに対するアクション実行パス状態を有する状態定義レコード群を抽出し、処理対象レコードにおける前イベントに記述されたイベントをイベント欄に有する状態定義レコードのアクション実行パス状態欄に記載されたアクション実行パス状態に一致するインデックスを有する行と、処理対象レコードのイベント欄に記載されたイベントに一致するインデックスを有する列との交点となるセルである処理対象セルの状態欄に、処理対象レコードのアクション実行パス状態欄に記載されているアクション実行パス状態を書き込み、処理対象レコードのアクション系列欄にアクションの記述があれば、そのアクションを上記処理対象セルのアクション欄に書き込むことにより、状態遷移表を生成する請求項１又は２に記載の状態遷移表生成装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本明細書に記載の実施の形態は、状態遷移表生成装置に関する。
【背景技術】
【０００２】
近年ソフトウェアが複雑化してきたことで、これまで以上に仕様の誤りが混入し易くなり、また人の手では仕様を網羅した検証が困難になってきている状況にある。その解決法として、形式的手法の一つであるモデル検査が着目され、モデル検査の実適用も進んでおり、人の手では発見しづらい不適合事例を発見し効果を上げている。
【０００３】
但し、上記モデル検査を実行する装置であるモデル検査器を利用するためには、専門的スキルやノウハウが必要となる。このため、モデル検査をより効率的に導入し易くするために、状態遷移図、状態遷移表、フローチャート等の仕様書からモデル検査器特有の言語を自動生成し、検査できるような支援ツールが開発されている。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２００７−１１６０５号公報
【特許文献２】特開２００８−１９８１０３号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
従来の支援ツールでは、入力情報として特定の表現（図又は仕様情報）のみをサポートしている。従って利用する支援ツールがどのような形式の入力仕様をサポートしているかによって、利用制限がかかってしまう。例えば、仕様を主にフローチャートで記述している場合は、状態遷移図/状態遷移表ベースの支援ソフトは利用できないという問題点があった。
【０００６】
本発明の目的は、フローチャートのような時系列の順序形式で記述された仕様書に対応する状態遷移表を作成するが、当該状態遷移表を用いたモデル検査を行った結果がフローチャートとの対応関係を維持し、仕様の誤りを容易に発見することを可能とする点にある。
【課題を解決するための手段】
【０００７】
一の実施の形態によれば、状態遷移表生成装置が提案される。この状態遷移表生成装置は、第１の生成手段と、第２の生成手段とを有する。
第１の生成手段は、入出力順序系列仕様を表すデータにおける条件分岐と処理に、イベント及びアクションを特定する情報を付し、分岐の無い一本のパスにアクション実行パス状態を特定する情報を付し、一つのアクション実行パス状態について一つのレコードを有し、各レコードはイベント、前イベント、アクション系列を有する情報である状態定義レコード表を生成する。
【０００８】
第２の生成手段は、前記状態定義レコード表に基づいて、前記状態定義レコード表に含まれるアクション実行パス状態ごとに一つのレコードを有し、各レコードは、前記状態定義レコード表に含まれる各イベントに対応するフィールドを有する情報である状態遷移表を生成する。
【図面の簡単な説明】
【０００９】
【図１】状態遷移表生成装置及び、この状態遷移表生成装置によって出力される状態遷移表を用いたモデル検査の流れを示した図
【図２】状態遷移表生成装置の構成例を示す機能ブロック図
【図３Ａ】状態定義レコード表生成処理の例を示したフローチャート
【図３Ｂ】図３Ａに続く状態定義レコード表生成処理の例を示したフローチャート
【図４】状態定義レコード表の元となる入出力順序系列仕様であるフローチャート
【図５】図４の処理対象フローチャートから生成された状態定義レコード表の例を示した図
【図６】状態遷移表生成処理の一例を示したフローチャート
【図７】本実施の形態の状態定義レコード表生成部が生成した状態定義レコード表の一例を示す図
【図８】図１７に示した状態遷移表を完成させる過程を示した図
【図９】図８に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１０】図９に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１１】図１０に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１２】図１１に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１３】図１２に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１４】図１３に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１５】図１４に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１６】図１５に続く、図１７に示した状態遷移表を完成させる過程を示した図
【図１７】図７に示した状態定義レコード表に基づいて、本実施の形態の状態遷移表生成部が生成した状態遷移表の例を示す図
【図１８】状態定義レコード表生成処理を実行することによって、図１７のフローチャートから生成された状態定義レコード表の一例を示す図
【図１９】状態遷移表生成処理によって図１８の状態定義レコードから生成された状態遷移表の例を示す図
【図２０】「イベント/アクション定義レコード」の一例を示した図
【図２１】状態遷移表生成装置の入力となるソースコードの一例を示す図
【図２２】図２１のソースコードにイベント及びアクションのラベルが付された状態を示す図
【図２３】状態定義レコード表生成処理（図３参照）を実行した結果得られる状態定義レコード表の例を示す図
【図２４】図２３に示した状態定義レコード表に基づいて、状態遷移表生成処理（図６参照）を実行した結果得られる状態遷移表の例を示す図
【図２５】第２の実施の形態にかかる状態遷移表生成装置の構成例を示すブロック図
【図２６】状態定義レコード生成部の動作である状態定義レコード生成処理の一例を示すフローチャート
【図２７】図２６に続くフローチャート
【図２８】本具体例において上記状態定義レコード表の元となる入出力順序系列仕様であるフローチャートを示す図
【図２９】図２８の処理対象フローチャートから生成された状態定義レコード表の例を示した図
【図３０】図２９に示した状態定義レコード表のデータから生成された状態遷移表の例を示す図
【図３１】ＩＰアドレスの割り当てを行う処理の例を示したシーケンス図
【図３２】クライアントであるＰＣ−１の処理フローチャートの例を示す図
【図３３】状態名（アクション実行パス状態）が付された図３２のフローチャートを示す図
【図３４】フローチャート（入出力順序系列仕様１０）から状態遷移表生成装置が生成した状態遷移表を状態遷移図に示した図
【図３５】ＤＨＣＰサーバであるＰＣ−３の処理フローチャートの例を示す図
【図３６】状態名（アクション実行パス状態）が付された図３５のフローチャートを示す図
【図３７】図３２のフローチャート（入出力順序系列仕様１０）から状態遷移表生成装置が生成した状態遷移表を状態遷移図に示した図
【発明を実施するための形態】
【００１０】
以下、図面を参照して本発明の実施の形態に係る状態遷移表生成装置を説明する。
[第１の実施の形態]
【００１１】
図１は、第１の実施の形態にかかる状態遷移表生成装置及び、この状態遷移表生成装置によって出力される状態遷移表を用いたモデル検査の流れを示した図である。
モデル検査の実施を行うユーザ（或いはオペレータなど、以下同じ）は、まず入出力順序系列仕様を用意する。ここで、「入出力順序系列仕様」とは、時系列の順序形式で記述された仕様書をいい、例えばフローチャートなどである。
【００１２】
ユーザは入出力順序系列仕様１０を状態遷移表生成装置１１に入力する。状態遷移表生成装置１１は、入出力順序系列仕様１０のデータを状態遷移表生成処理方法によって処理し、その処理結果として状態遷移表１２を生成し、出力する。
ユーザは状態遷移表１２に基づいて検査用コード１３を作成するとともに、検査式１４を作成する。ユーザは検査用コード１３及び検査式１４をモデル検査器１５に入力する。
【００１３】
モデル検査器１５はモデル検査処理を実行し、反例１６を出力する。ユーザは反例を解析することにより、問題点を発見し、検査用コード１３を修正し、この修正済みの検査用コード１３をモデル検査器１５によってさらに検査し、問題点をつぶすように、検査用コード１３の改善を行う。
【００１４】
図２は、状態遷移表生成装置１１の構成例を示す機能ブロック図である。なお、図２に示した各構成要素は、状態遷移表生成装置１１を機能ごとのまとまりとしてとらえた要素であって、実際の状態遷移表生成装置１１が各構成様相に相当するハードウエア（回路、モジュール、ユニットなど）を備えていることを必要とすることを示すものではない。
【００１５】
状態遷移表生成装置１１は、例えばコンピュータ、ワークステーションなどの情報処理装置によって実現される装置である。この情報処理装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読出し専用メモリ（ＲＯＭ）、入出力装置（Ｉ／Ｏ）、及び必要な場合にはハードディスク装置等の外部記憶装置を具備している装置である。
【００１６】
状態遷移表生成装置１１は、入出力順序系列仕様記憶部２１と、本実施の形態のだ第の生成手段に相当する状態定義レコード表生成部２２と、本実施の形態の第１の生成手段に相当する状態遷移表生成部２３と、イベント／アクション定義レコード表生成部２４とを有する。入出力順序系列仕様記憶部２１は状態定義レコード表生成部２２に接続されており、状態定義レコード表生成部２２は状態遷移表生成部２３に接続されており、イベント／アクション定義レコード表生成部２４は状態遷移表生成部２３に接続されている。ここで「接続されている」とは、データ、情報、命令などの授受が可能な状態になっていることをいい、配線で連結されているような物理的な接続に限られる意味ではない。
【００１７】
入出力順序系列仕様記憶部２１は、ユーザによって入力された入出力順序系列仕様を記憶する機能を有する。入出力順序系列仕様は状態定義レコード表生成部２２が読み取り可能な形式、フォーマットなどであればどのようなデータとして保存されていてもよい。
【００１８】
状態定義レコード表生成部２２は、入出力順序系列仕様を表すデータを入出力順序系列仕様記憶部２１から受信し、後述する状態定義レコード表生成処理を実行することにより状態定義レコード表を表すデータを生成し、出力する機能を有する。
【００１９】
状態遷移表生成部２３は、状態定義レコード表生成部２２から状態定義レコード生成部２２から状態定義レコード表を表すデータを受信し、後述する状態遷移表生成処理を実行することにより、状態遷移表を表すデータを生成し、出力する機能を有する。
【００２０】
イベント／アクション定義レコード表生成部２４は、入出力順序系列仕様に含まれるイベント、アクションに付したラベル（符号）と、当該ラベルの内容を示す文や単語とを対応付けしたデータであるイベント／アクション定義レコード表を生成し、記憶する機能を有する。
【００２１】
[状態定義レコード表生成処理]
以下に、図３Ａ，図３Ｂを参照しながら状態定義レコード表生成処理の例を説明する。図３Ａは、状態定義レコード表生成処理の例を示したフローチャート、図３Ｂは図３Ａに続くフローチャートである。なお、本説明においては、入出力順序系列仕様１０はフローチャートであるものとして説明する。
【００２２】
まず、状態定義レコード表生成部２２は、フローチャートの条件分岐、処理の各要素にそれぞれイベントとアクションの番号付けをする（Ｓ１０）。すなわち、条件分岐処理にはイベントの番号付けをし、アクション（通常処理）にはアクションの番号付けを行う。
【００２３】
次に、状態定義レコード表生成部２２は、状態定義レコード表を生成する。状態定義レコード表は、一つのアクション実行パス状態について一つのレコードを有し、各レコードは「イベント」、「前イベント」、「アクション系列」という３つのフィールドを有する情報である。状態定義レコード表生成部２２は、フローチャートの最初の要素である「Start」を読み取ると、アクション実行パス状態欄に「State0」を格納し、且つそのイベント欄にイベント名「Start」と格納したレコードを状態定義レコード表に加える（Ｓ２０）。
【００２４】
次に、状態定義レコード表生成部２２は、「終了（End）」以外の全ての要素を読み込み済みで且つ状態定義済みか否かを判定する（Ｓ３０）。「終了（End）」以外の全ての要素を読み込み済みである場合には、状態定義レコード表生成部２２は現在の状態数を含む状態名をアクション実行パス状態欄に格納し、且つイベント欄に「End」を格納した新たな状態定義レコードを生成し、状態定義レコード表に追加する（Ｓ１１０）。
次に、状態定義レコード表生成部２２は、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（Ｓ１２０)。
一方、「終了（End）」以外の全ての要素を読み込み済みでない場合（Ｓ３０、Ｎｏ）、状態定義レコード表生成部２２は、フローチャートの連結部分から一要素を読み取る（Ｓ４０）。
【００２５】
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する（Ｓ５０）。その要素が条件分岐ではないと判定した場合（Ｓ５０，Ｎｏ）、状態定義レコード表生成部２２は、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号（ラベルともいう）を状態定義レコード表に登録する（Ｓ６０）。その後、先に述べたステップＳ３０に戻り、処理を続行する。
【００２６】
一方、ステップＳ５０においてその要素が条件分岐であると判定した場合（Ｓ５０，Ｙｅｓ）、状態定義レコード表生成部２２は、当該条件分岐によって生じる状態を定義する状態名を状態定義レコード表に登録する（Ｓ７０）。ここで「状態」とは、アクション実行パスであって、ある条件分岐から次の条件分岐に至るまでのフローチャート上の経路（パス）に相当する。本例では状態名は「State[状態レコード数]」というフォーマットで記述するものとする。
なお、本例では、上記経路を状態として扱っているが、条件分岐ごと状態として扱っても実施可能である。この場合経路は状態の区別に関係しない。
【００２７】
次に、状態定義レコード表生成部２２は、その条件分岐がイベントとして状態定義レコード表に登録済みであるか否かを判定する（Ｓ８０）。その条件分岐がイベントとして状態定義レコード表に登録済みではないと判定した場合（Ｓ８０、Ｎｏ）、状態定義レコード表生成部２２は、状態定義レコード表に新たに状態定義レコードを2つ作成し、その条件分岐の「TRUE」に対応するイベントを一方のレコードのイベント欄に登録し、他方のレコードにその条件分岐の「FALSE」に対応するイベントを登録する（Ｓ９０）。
【００２８】
次に、状態定義レコード表生成部２２は、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（Ｓ１００）。その後ステップＳ３０に戻り、処理を続行する。
【００２９】
一方、ステップＳ８０においてその条件分岐がイベントとして状態定義レコード表に登録済みであると判定した場合（Ｓ８０，Ｙｅｓ）、状態定義レコード表生成部２２は、ステップＳ９０を行うこと無く、ステップＳ１００を実行する。
以上で状態定義レコード表生成処理の説明を終了する。
【００３０】
[具体例]
上記状態定義レコード表生成処理の具体例を示す。図４は、本具体例において上記状態定義レコード表の元となる入出力順序系列仕様１０であるフローチャート（「処理対象フローチャート」と呼ぶ）である。図５は、図４の処理対象フローチャートから生成された状態定義レコード表の例を示した図である。以下、図３、図４、図５を参照しながら状態定義レコード表生成処理の具体例を説明する。
【００３１】
処理対象フローチャートの内容は以下の通りである。まず、初めに第1の条件分岐であるステップＳ１０１がある。条件分岐ステップＳ１０１の「Ｔｒｕｅ」に対応するアクションであるステップＳ１０２があり、ステップＳ１０２に続く別のアクションであるステップＳ１０２がある。また、条件分岐ステップＳ１０１の「Ｆａｌｓｅ」に対応するアクションはステップＳ１０３である。
【００３２】
ステップＳ１０３に続いて第2の条件分岐であるステップＳ１０４がある。条件分岐ステップＳ１０４の「Ｔｒｕｅ」に対応するアクションとしてアクションであるステップＳ１０５があり、ステップＳ１０５の後この処理対象フローチャートの処理は「Ｅｎｄ」に到達する。また、第２の条件分岐のステップＳ１０４の「Ｆａｌｓｅ」に対応するのは、「Ｅｎｄ」となる。
【００３３】
さて、この処理対象フローチャートに基づいて状態定義レコード表の作成処理を行う。まず、状態定義レコード表生成部２２は、フローチャートの条件分岐、処理の各要素にそれぞれイベントとアクションの番号付けをする（図３、Ｓ１０）。具体的には、第1の条件分岐Ｓ１０１にはイベント番号「Ｅ１」を付与し、第２の条件分岐Ｓ１０４にはイベント番号「Ｅ２」を付与する。また、アクションＳ１０２、Ｓ１０３、Ｓ１０４にはそれぞれアクション番号「Ａ１」、「Ａ２」、「Ａ３」を付与する。
【００３４】
次に、状態定義レコード表生成部２２は、状態定義レコード表を生成し、当該状態定義レコード表の第１のレコードとして、アクション実行パス状態欄に[State0]が格納され、イベント欄に[Start]が格納されたレコードを加える（図３、Ｓ２０）。
【００３５】
次に、状態定義レコード表生成部２２は、「終了（End）」以外の全ての要素を読み込み済みで且つ状態定義済みか否かを判定する（図３、Ｓ３０）。この具体例では、まだいずれの要素も読み込んでいないので、判定は「Ｎｏ」としてステップＳ４０に移行する。
【００３６】
次に、状態定義レコード表生成部２２は、処理対象フローチャートの連結部分から一要素を読み取る（図３、Ｓ４０）。この例では処理対象フローチャートの要素「Start」を読み込む。
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する（図３、Ｓ５０）。この例では要素「Start」は条件分岐ではないと判定される（図３、Ｓ５０、Ｎｏ）。
【００３７】
次に、状態定義レコード表生成部２２は、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号を状態定義レコード表に登録する（図３、Ｓ６０）。具体的には、図５に示した状態定義レコード表の第１行の「アクション実行パス状態」欄に「State0」と記述し、同第1行の「イベント」欄に読み取った要素の要素番号である「Start」を記述する。
【００３８】
次に、状態定義レコード表生成部２２は、ステップＳ３０の判定後、処理対象フローチャートの連結部分から次の一要素を読み取る（図３、Ｓ４０）。この例では処理対象フローチャートの要素「Ｅ１」を読み込む。
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する。この例では要素「Ｅ１」は条件分岐であると判定される（図３、Ｓ５０、Ｙｅｓ）。
【００３９】
次に、状態定義レコード表生成部２２は、当該条件分岐によって生じる状態を定義する状態名を決定する（図３、Ｓ７０）。この例では、状態定義レコード表生成部２２は、条件分岐「Ｅ１」の「Ｔｒｕｅ」における経路（Ｅ１からＡ１，Ａ２を経由してＥ２に至る経路）を状態名「State1」と定め、また条件分岐「Ｅ１」の「False」における経路（Ｅ１からＡ２を経由してＥ２に至る経路）を状態名「State2」と定める。
【００４０】
次に、状態定義レコード表生成部２２は、その条件分岐がイベントとして状態定義レコード表に登録済みであるか否かを判定する（図３、Ｓ８０）。この例では、条件分岐「Ｅ１」は未だ状態定義レコード表に登録済みではないと判定し（図３、Ｓ８０、Ｎｏ）、ステップＳ９０に移行する。
【００４１】
ステップＳ９０において、状態定義レコード表生成部２２は、状態定義レコード表に新たに状態定義レコードを2つ作成し、その条件分岐の「True」に対応するイベントを一方のレコードのイベント欄に登録し、他方のレコードにその条件分岐の「False」に対応するイベントを登録する。この例では、状態定義レコード表生成部２２は、図５の状態定義レコード表において、第２行と第３行を作成し、第２行の「アクション実行パス状態」欄に「State1」を記述するとともに「イベント」欄に「E1[True]」を記述する。またさらに状態定義レコード表生成部２２は、第３行の「アクション実行パス状態」欄に「State2」と記述するとともに「イベント」欄に「E1[False]」を記述する。
【００４２】
次に、状態定義レコード表生成部２２は、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（図３、Ｓ１００）。この例では、状態定義レコード表生成部２２は、直前に登録したイベントである「E1[True]」（第２行）、「E1[False]」（第３行）に対応する「前イベント」欄に、直前に状態を定義したレコード（第１行）の「イベント」欄に記述されたイベント「Start」を記述する。
【００４３】
次に、状態定義レコード表生成部２２は、ステップＳ３０に戻りその後ステップＳ４０において、要素「Ｅ１」の次の要素「Ａ１」を読み取る（図３、Ｓ４０）。
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する。この例では要素「Ａ１」は条件分岐ではないと判定される（図３、Ｓ５０、Ｎｏ）。
【００４４】
次に、状態定義レコード表生成部２２は、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号を状態定義レコード表に登録する（図３、Ｓ６０）。具体的には、図５に示した状態定義レコード表の第２行の「アクション系列」欄に「Ａ１」と記述する。
【００４５】
次に、状態定義レコード表生成部２２は、ステップＳ３０に戻りその後ステップＳ４０において、要素「Ａ１」の次の要素「Ａ２」を読み取る（図３、Ｓ４０）。
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する（図３、Ｓ５０）。この例では要素「Ａ２」は条件分岐ではないと判定される（図３、Ｓ５０、Ｎｏ）。
【００４６】
次に、状態定義レコード表生成部２２は、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号を状態定義レコード表に登録する（図３、Ｓ６０）。具体的には、図５に示した状態定義レコード表の第２行の「アクション系列」欄に「Ａ２」を追加するように記述する。
【００４７】
次に、状態定義レコード表生成部２２は、ステップＳ３０に戻りその後ステップＳ４０において、処理対象フローチャートにおける要素「Ａ２」の次の要素「Ｅ２」を読み取る（図３、Ｓ４０）。
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する（図３、Ｓ５０）。この例では要素「Ｅ２」は条件分岐であると判定される（図３、Ｓ５０、Ｙｅｓ）。
【００４８】
次に、状態定義レコード表生成部２２は、当該条件分岐によって生じる状態を定義する状態名を決定する（Ｓ７０）。この例では、状態定義レコード表生成部２２は、条件分岐「Ｅ２」の「True」における経路（Ｅ２からＡ３を経由してＥｎｄに至る経路）を状態名「State3」と定め、また条件分岐「Ｅ２」の「False」における経路（Ｅ２からＥｎｄに至る経路）を状態名「State４」と定める。
【００４９】
次に、状態定義レコード表生成部２２は、その条件分岐がイベントとして状態定義レコード表に登録済みであるか否かを判定する（図３、Ｓ８０）。この例では、条件分岐「Ｅ２」は未だ状態定義レコード表に登録済みではないと判定し（図３、Ｓ８０、Ｎｏ）、ステップＳ９０に移行する。
【００５０】
ステップＳ９０において、状態定義レコード表生成部２２は、図５に示す状態定義レコード表に新たに状態定義レコードを2つ追加し、その条件分岐の「True」に対応するイベントを一方のレコードのイベント欄に登録し、他方のレコードにその条件分岐の「False」に対応するイベントを登録する。この例では、状態定義レコード表生成部２２は、状態定義レコード表に第４行と第５行を作成し、第４行の「アクション実行パス状態」欄に「State3」を記述するとともに「イベント」欄に「E2[True]」を記述する。またさらに状態定義レコード表生成部２２は、第５行の「アクション実行パス状態」欄に「State4」と記述するとともに「イベント」欄に「E2[False]」を記述する。
【００５１】
次に、状態定義レコード表生成部２２は、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（図３、Ｓ１００)。この例では、状態定義レコード表生成部２２は、第４行及び第５行の登録の直前に登録したレコード（第2行、第3行に相当するレコード）のイベント欄に記述された「E1[True]」（第２行）及び「E1[False]」（第３行）を第４行、第５行の「前イベント」欄に記述する。
【００５２】
次に、状態定義レコード表生成部２２は、ステップＳ３０に戻りその後ステップＳ４０において、要素「Ｅ２」の次の要素「Ａ３」を読み取る（図３、Ｓ４０）。
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する（図３、Ｓ５０）。この例では要素「Ａ３」は条件分岐ではないと判定される（Ｓ５０、Ｎｏ）。
【００５３】
次に、状態定義レコード表生成部２２は、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号を状態定義レコード表に登録する（図３、Ｓ６０）。具体的には、図５に示した状態定義レコード表の第４行の「アクション系列」欄に「Ａ３」を記述する。
【００５４】
次に、状態定義レコード表生成部２２は、ステップＳ３０に戻り終了（Ｅｎｄ）以外の全ての要素を読み込み済みか否かを判定する（Ｓ３０）。この例では、状態定義レコード表生成部２２は、終了（Ｅｎｄ）以外の全ての要素を読み込み済みであると判定し（Ｓ３０、Ｙｅｓ）、図３ＢのステップＳ１１０に進む。
【００５５】
ステップＳ１１０において、状態定義レコード表生成部２２は現在の状態数を含む状態名をアクション実行パス状態欄に格納し、且つイベント欄に「End」を格納した新たな状態定義レコードを生成し、状態定義レコード表に追加する（Ｓ１１０）。この例では、第６行のレコードに相当する。
【００５６】
次に、状態定義レコード表生成部２２は、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（Ｓ１２０)。この例では、状態定義レコード表生成部２２は、第６行の登録の直前に登録したレコード（第４行、第５行に相当するレコード）のイベント欄に記述された「E2[True]」（第４行）及び「E2[False]」（第５行）を第６行の「前イベント」欄に記述する。図4に示したフローチャートに基づく状態定義レコード表が完成する。
以上で、状態定義レコード表生成処理の説明を終了する。
【００５７】
[状態遷移表生成処理]  
次に、状態定義レコード表から状態遷移表を生成する処理である、状態遷移表生成処理について説明する。図６は、状態遷移表生成処理の一例を示したフローチャートである。以下、このフローチャートを参照しながら状態遷移表生成処理について説明する。
【００５８】
状態定義レコード表生成部２２によって生成された状態定義レコード表を取得した状態遷移表生成部２３は、状態定義レコード表の「アクション実行パス状態」欄に記述された内容を、状態遷移表の各行のインデックスとして状態遷移表に記述し、且つ状態定義レコード表の「イベント」欄に記述された内容を各列のインデックスとして状態遷移表に記述する（Ｓ２０１）。
次に、状態遷移表生成部２３は、状態定義レコード表の最初の状態定義レコード(状態定義レコード表の第1行に相当する）を読み込む（Ｓ２０２）
【００５９】
次に、状態遷移表生成部２３は、取得した状態定義レコード表の全ての状態定義レコードを読み終えたか否かを判定する（Ｓ２０３）。全ての状態定義レコードを読み終えたと判定した場合（Ｓ２０３、Ｙｅｓ）、状態遷移表生成部２３は、状態遷移表の空いているセルの全てに空欄であることを示す所定の情報、例えば記号「／」(スラッシュ)を書き込む（ステップＳ２１１）。このステップＳ２１１終了後、状態遷移表生成部２３は状態遷移表生成処理を終了する。一方、ステップＳ２０３において全ての状態定義レコードを読み終えていないと判定した場合（Ｓ２０３、Ｎｏ）、状態遷移表生成部２３は、現在処理している状態定義レコード（以下、「処理対象レコード」と呼ぶ）の「アクション実行パス状態」欄に記述されている情報が「State0」でないか否かを判定する（Ｓ２０４）。
【００６０】
ステップＳ２０４において処理対象レコードの「アクション実行パス状態」欄の記述が「State0」であると判定した場合（Ｓ２０４、Ｎｏ）、状態遷移表生成部２３は次の状態定義レコードを処理対象レコードとする（Ｓ２０５）。その後ステップＳ２０３に戻る。
【００６１】
一方、ステップＳ２０４において処理対象レコードの「アクション実行パス状態」が「State0」でないと判定した場合（Ｓ２０４、Ｙｅｓ）、状態遷移表生成部２３は処理対象レコードを読み取る（Ｓ２０６）。
【００６２】
状態遷移表生成部２３はＳ２０６において読み取った処理対象レコードの「前イベント」欄に何らかのイベントが記述されているか否かを判定する（Ｓ２０７）。ステップＳ２０７において、「前イベント」欄に何のイベントも記述されていないと判定した場合（Ｓ２０７、Ｎｏ）、状態遷移表生成部２３は、前イベントに対するアクション実行パス状態を「State0」に決定する（Ｓ２０８）。この「State0」は後述する「処理対象セル」を決定するための情報として用いられる。
【００６３】
ステップＳ２０８実行後、状態遷移表生成部２３は、状態定義レコード表から、前イベントに対するアクション実行パス状態を有する状態定義レコード群を抽出する（Ｓ２０９）。より具体的には、状態遷移表生成部２３は、状態定義レコード表の全ての状態定義レコードのうち、処理対象レコードの「前イベント」欄に記載されたイベントと同一のイベントを「イベント」欄に有する状態定義レコードを全て抽出する。この抽出された行を抽出レコードと呼ぶこととする。また、処理対象レコードにおいて「前イベント」欄に記載が無い場合は、状態遷移表における「Init」行を、処理対象セルを定めるための行とする。
【００６４】
次に、状態遷移表生成部２３は、前イベントに対するアクション実行パス状態群に対するイベントの状態遷移先として、イベントに対するアクション実行パス状態を定義する（Ｓ２１０）。より具体的には、状態遷移表生成部２３は、状態遷移表において、処理対象レコードにおける「前イベント」に記述されたイベントを「イベント」欄に有する状態定義レコードの「アクション実行パス状態」欄に記載されたアクション実行パス状態に一致するインデックスを有する行と、処理対象レコードの「イベント」欄に記載されたイベントに一致するインデックスを有する列との交点となるセル（処理対象セルと呼ぶ）の状態欄に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態を書き込む。また、処理対象レコードの「アクション系列」欄にアクションの記述があれば、そのアクションを上記処理対象セルのアクション欄に書き込む。
ステップＳ２１０終了後、状態遷移表生成部２３はステップＳ２０５に戻る。
【００６５】
一方、前述のステップＳ２０７において、「前イベント」欄にイベントが記述されていると判定した場合（Ｓ２０７、Ｙｅｓ）、状態遷移表生成部２３は直ちにステップＳ２０９に進む。  
以上で、状態遷移表作成処理の説明を終了する。
【００６６】
[状態遷移表作成処理の具体例]
次に、上述した状態遷移表作成処理について、具体例を挙げて説明する。図７は、本実施の形態の状態定義レコード表生成部２２が生成した状態定義レコード表の一例を示す図であり、図１７は図７に示した状態定義レコード表に基づいて、本実施の形態の状態遷移表生成部２３が生成した状態遷移表の例を示す図である。また、図８から図１６は図１７に示した状態遷移表を完成させる過程を示した図である。以下、状態遷移表作成処理によりどのように図７に示した状態定義レコード表から図１７に示した状態遷移表が生成されるかを図６から図１7を参照しながら説明する。
【００６７】
状態定義レコード表生成部２２によって生成された状態定義レコード表を取得した状態遷移表生成部２３は、図７の状態定義レコード表の「アクション実行パス状態」欄(最左列の各セル)に記述された内容である「State0」、「State1」、「State2」、「State3」、「State4」、「State5」及びこれらに加えて「Init」を、状態遷移表の最左列の各セルに記述し、また状態定義レコード表の「イベント」欄（左端から２番目の列の各セル）に記述された内容である「Start」、「E1[true]」、「E1[false]」、「E2[true]」、「E2[false]」、「End」を状態遷移表の最上行の各セルに各列のインデックスとして記述する（図６、Ｓ２０１参照）。
【００６８】
次に、状態遷移表生成部２３は、状態定義レコード表の第１行の状態定義レコードを読む（図６、Ｓ２０２）。第１行の状態定義レコードはこの時点での「処理対象レコード」となる。図８は、状態とイベントがインデックスとして記述される前の状態遷移表の例を示した図、図９は図８の状態遷移表に状態とイベントがインデックスとして記述された状態を示した図である。
【００６９】
次に、状態遷移表生成部２３は、状態定義レコード表の全ての状態定義レコードを読み終えたか否かを判定する（図６、Ｓ２０３）。本具体例では、状態遷移表生成部２３は全ての行を読み終えていないと判定する（図６、Ｓ２０３、Ｎｏ）。
【００７０】
次に状態遷移表生成部２３は処理対象レコードの「アクション実行パス状態」のセルに記述されている情報が「State0」でないか否かを判定する（図６、Ｓ２０４）。本具体例では、状態遷移表生成部２３はステップＳ２０３において処理対象レコードにおける「アクション実行パス状態」欄のセルに記述された情報は「State0」であると判定し、ステップＳ２０５に進む（Ｓ２０４、Ｎｏ）。ここで、状態遷移表生成部２３はアクション実行パス状態に「Init」が記載された行と、処理対象レコードの「イベント」欄に記載されたイベント「Start」に一致するインデックスを有する列との交点となるセル（処理対象セルと呼ぶ）の状態欄に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State0」を書き込む。  図１０に、図９の状態の後上記処理で「State0」が書き込まれた状態の状態遷移表の例を示す。
【００７１】
[状態定義レコード表、第２行の処理]
ステップＳ２０５では、状態遷移表生成部２３は状態定義レコード表の次のレコードを処理対象レコードにする（図６、Ｓ２０５）。本具体例では、図７の状態定義レコード表の第２行、「アクション実行パス状態」欄のセルが「State1」である状態定義レコードが新たな処理対象レコードに決定される。
【００７２】
次に、状態遷移表生成部２３は、取得した状態定義レコード表の全ての行（レコード）を読み終えたか否かを判定する（図６、Ｓ２０３）。本具体例では、状態遷移表生成部２３は全ての行を読み終えていないと判定する（図６、Ｓ２０３、Ｎｏ）。
【００７３】
次に状態遷移表生成部２３は状態定義レコード表の処理対象レコードの「アクション実行パス状態」のセルに記述されている情報が「State0」でないか否かを判定する（図６、Ｓ２０３）。本具体例では、処理対象レコードの「アクション実行パス状態」のセルは「State1」であるので、ステップＳ２０６に進む。ステップＳ２０６において、状態遷移表生成部２３は処理対象レコードを読む。本具体例では、状態定義レコード表の第２行、「アクション実行パス状態」欄のセルが「State1」である状態定義レコードが読み取られる。
【００７４】
次に、状態遷移表生成部２３は、処理対象レコードにおける「前イベント」欄に記述されたイベントがあるか否かを判定する（図６、Ｓ２０７）。本具体例では、状態定義レコード表の第２行の「前イベント」欄には、イベント「Start」の記述があるので、ステップＳ２０９へと進む。
【００７５】
状態遷移表生成部２３は、状態定義レコード表から、前イベントに対するアクション実行パス状態を有する状態定義レコード群を抽出する（図６、Ｓ２０９）。抽出されたレコード群を「抽出レコード群」と呼ぶこととする。本具体例では、状態定義レコード表においてイベント「Start」が「イベント」欄に記述されている状態定義レコードが抽出され、抽出レコード群は第１行の状態定義レコードのみである。
【００７６】
次に、状態遷移表生成部２３は、状態遷移表において、抽出レコード群の「アクション実行パス状態」欄に記載されたアクション実行パス状態に一致するインデックスを有する行と、処理対象レコードの「イベント」欄に記載されたイベントに一致するインデックスを有する列との交点となるセル（処理対象セルと呼ぶ）の状態欄に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態を書き込む（図６、Ｓ２１０）のであるが、抽出レコードである第１行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State0」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「E1[True]」である。よって、状態遷移表における処理対象セルは、「State0」をインデックスとする第２行と、「E1[True]」をインデックスとする左端から第２列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State1」を書き込む。さらに状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクション「A1,A2」を上記処理対象セルのアクション欄（セル内下側）に書き込む（図６、Ｓ２１０参照）。状態「State1」及びアクション「A1,A2」が処理対象セルに書き込まれた状態の状態遷移表の例を図１１に示す。
【００７７】
[状態定義レコード表、第３行の処理]
次に状態遷移表生成部２３はステップＳ２０５に進み、状態定義レコード表の次のレコードを処理対象レコードにする（図６、Ｓ２０５）。本具体例では、図５の状態定義レコード表の第３行、「アクション実行パス状態」欄のセルが「State2」である状態定義レコードが新たな処理対象レコードに決定される。
【００７８】
次に、状態遷移表生成部２３は、取得した状態定義レコード表の全ての行（レコード）を読み終えたか否かを判定する（図６、Ｓ２０３）。本具体例では、状態遷移表生成部２３は全ての行を読み終えていないと判定する（Ｓ２０３、Ｎｏ）。
【００７９】
次に状態遷移表生成部２３は状態定義レコード表の処理対象レコード「アクション実行パス状態」のセルに記述されている情報が「State0」でないか否かを判定する（図６、Ｓ２０３）。本具体例では、処理対象レコードの「アクション実行パス状態」欄の記述は「State2」であるので、ステップＳ２０６に進む。ステップＳ２０６において、状態遷移表生成部２３は処理対象レコードを読む。本具体例では、状態定義レコード表の第３行、「アクション実行パス状態」欄のセルが「State2」である状態定義レコードが読み取られる。
【００８０】
次に、状態遷移表生成部２３は、処理対象レコードにおける「前イベント」欄に記述されたイベントがあるか否かを判定する（Ｓ２０７）。本具体例では、状態定義レコード表の第３行の「前イベント」欄には、イベント「Start」の記述があるので、ステップＳ２０９へと進む。
【００８１】
状態遷移表生成部２３は、状態定義レコード表から、前イベントに対するアクション実行パス状態を有する状態定義レコード群を抽出する（図６、Ｓ２０９）。本具体例では、状態定義レコード表においてイベント「Start」が「イベント」欄に記述されている状態定義レコードが抽出レコード群として抽出され、抽出レコード群は第１行の状態定義レコードのみである。
【００８２】
次に、状態遷移表生成部２３は、状態遷移表において、抽出レコード群の「アクション実行パス状態」欄に記載されたアクション実行パス状態に一致するインデックスを有する行と、処理対象レコードの「イベント」欄に記載されたイベントに一致するインデックスを有する列との交点となる処理対象セルの状態欄に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態を書き込み、同処理対象セルのアクション欄に、処理対象レコードの「アクション系列」欄に記載されたアクションを記述する（Ｓ２１０参照）。本具体例では、抽出レコード群は状態定義レコード表の第１行のみであり、その第１行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State0」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「E1[False]」である。よって、状態遷移表における処理対象セルは、「State0」をインデックスとする第２行と、「E1[False]」をインデックスとする左端から第３列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State2」を書き込む。状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクションを上記処理対象セルのアクション欄（セル内下側）に書き込むのであるが、処理対象レコード「アクション系列」欄は空欄であるので、上記処理対象セルのアクション欄は空欄のままとなる。（Ｓ２１０参照）。処理対象セルに上記「State2」が記述され、アクション欄は空欄のままとされた状態の状態遷移表の例を図12に示す。
【００８３】
[状態定義レコード表、第４行の処理]
次に状態遷移表生成部２３はステップＳ２０５に進み、状態定義レコード表の次のレコードを処理対象レコードにする（図６、Ｓ２０５）。本具体例では、図５の状態定義レコード表の第４行、「アクション実行パス状態」欄のセルが「State3」である状態定義レコードが新たな処理対象レコードに決定される。
【００８４】
次に、状態遷移表生成部２３は、取得した状態定義レコード表の全ての行（レコード）を読み終えたか否かを判定する（図６、Ｓ２０３参照）。本具体例では、状態遷移表生成部２３は全ての行を読み終えていないと判定する（図６、Ｓ２０３、Ｎｏ）。
【００８５】
次に状態遷移表生成部２３は処理対象レコード「アクション実行パス状態」のセルに記述されている情報が「State0」でないか否かを判定する（図６、Ｓ２０３）。本具体例では、処理対象レコードの「アクション実行パス状態」欄の記述は「State3」であるので、ステップＳ２０６に進む。ステップＳ２０６において、状態遷移表生成部２３は処理対象レコードを読む。本具体例では、状態定義レコード表の第４行、「アクション実行パス状態」欄のセルが「State3」である状態定義レコードが読み取られる。
【００８６】
次に、状態遷移表生成部２３は、処理対象レコードにおける「前イベント」欄に記述されたイベントがあるか否かを判定する（図６、Ｓ２０７）。本具体例では、状態定義レコード表の第４行の「前イベント」欄には、イベント「E1[True]」及び「E1[False]」の記述があるので、ステップＳ２０９へと進む。
【００８７】
状態遷移表生成部２３は、状態定義レコード表から、前イベントに対するアクション実行パス状態を有する状態定義レコード群を抽出する（Ｓ２０９参照）。本具体例では、状態定義レコード表においてイベント「E1[True]」及び「E1[False]」が「イベント」欄に記述されている状態定義レコードが抽出され、抽出レコードは「E1[True]」について第２行の状態定義レコードのみ、「E1[False]」について第３行の状態定義レコードのみである。
【００８８】
次に、状態遷移表生成部２３は、状態遷移表において、抽出レコード群の「アクション実行パス状態」欄に記載されたアクション実行パス状態に一致するインデックスを有する行と、処理対象レコードの「イベント」欄に記載されたイベントに一致するインデックスを有する列との交点となる処理対象セルの状態欄に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態を書き込み、同処理対象セルのアクション欄に、処理対象レコードの「アクション系列」欄に記載されたアクションを記述する（図６、Ｓ２１０参照）。
【００８９】
状態定義レコード表において「E1[True]」についての抽出レコード群は第２行のみであり、その第２行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State1」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「E2[True]」である。よって、状態遷移表における処理対象セルは、「State1」をインデックスとする第３行と、「E2[True]」をインデックスとする左端から第４列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State3」を書き込む。さらに状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクションを上記処理対象セルのアクション欄（セル内下側）に書き込むのであるが、処理対象レコード「アクション系列」欄にはアクション「A3」が記述されているので、上記処理対象セルのアクション欄に「A3」を記述する。（Ｓ２１０参照）。
【００９０】
次に、もう一つのイベントである「E1[False]」についての抽出レコード群の処理に付いて述べる。状態定義レコード表において「E1[False]」についての抽出レコードは第３行のみであり、その第３行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State2」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「E2[True]」である。よって、状態遷移表における処理対象セルは、「State2」をインデックスとする第４行と、「E2[True]」をインデックスとする左端から第４列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State3」を書き込む。さらに状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクションを上記処理対象セルのアクション欄（セル内下側）に書き込むのであるが、処理対象レコード「アクション系列」欄にはアクションが記述されていないので、上記処理対象セルのアクション欄には何も書き込まれない。（Ｓ２１０参照）。上記状態定義レコード表、第４行の処理が終了した時点の状態遷移表の状態を図１３に示す。
【００９１】
[状態定義レコード表、第５行の処理]
次に状態遷移表生成部２３はステップＳ２０５に進み、状態定義レコード表の次のレコードを処理対象レコードにする（図６、Ｓ２０５）。本具体例では、図５の状態定義レコード表の第５行、「アクション実行パス状態」欄のセルが「State4」である状態定義レコードが新たな処理対象レコードに決定される。
【００９２】
次に、状態遷移表生成部２３は、状態定義レコード表の全ての行（レコード）を読み終えたか否かを判定する（図６、Ｓ２０３参照）。本具体例では、状態遷移表生成部２３は全ての行を読み終えていないと判定する（図６、Ｓ２０３、Ｎｏ）。
【００９３】
次に状態遷移表生成部２３は状態定義レコード表の処理対象レコード「アクション実行パス状態」のセルに記述されている情報が「State0」でないか否かを判定する（図６、Ｓ２０３）。本具体例では、処理対象レコードの「アクション実行パス状態」欄の記述は「State4」であるので、ステップＳ２０６６に進む。ステップＳ２０６において、状態遷移表生成部２３は処理対象レコードを読む。本具体例では、状態定義レコード表の第５行、「アクション実行パス状態」欄のセルが「State4」である状態定義レコードが読み取られる。
【００９４】
次に、状態遷移表生成部２３は、処理対象レコードにおける「前イベント」欄に記述されたイベントがあるか否かを判定する（Ｓ２０７）。本具体例では、状態定義レコード表の第５行の「前イベント」欄には、イベント「E1[True]」及び「E1[False]」の記述があるので、ステップＳ２０９へと進む（図６、Ｓ２０７、Ｙｅｓ）。
【００９５】
状態遷移表生成部２３は、状態定義レコード表から、前イベントに対するアクション実行パス状態を有する状態定義レコード群を抽出する（Ｓ２０９参照）。本具体例では、状態定義レコード表においてイベント「E1[True]」及び「E1[False]」が「イベント」欄に記述されている状態定義レコードが抽出され、「E1[True]」についての抽出レコード群は第２行の状態定義レコードのみ、「E1[False]」についての抽出レコード群は第３行の状態定義レコードのみである。
【００９６】
次に、状態遷移表生成部２３は、状態遷移表において、抽出レコードの「アクション実行パス状態」欄に記載されたアクション実行パス状態に一致するインデックスを有する行と、処理対象レコードの「イベント」欄に記載されたイベントに一致するインデックスを有する列との交点となる処理対象セルの状態欄に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態を書き込み、同処理対象セルのアクション欄に、処理対象レコードの「アクション系列」欄に記載されたアクションを記述する（図６、Ｓ２１０）。
【００９７】
状態定義レコード表において「E1[True]」についての抽出レコード群は第２行のみであり、その第２行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State1」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「E2[False]」である。よって、状態遷移表における処理対象セルは、「State1」をインデックスとする第３行と、「E2[False]」をインデックスとする左端から第５列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State4」を書き込む。さらに状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクションを上記処理対象セルのアクション欄（セル内下側）に書き込むのであるが、処理対象レコード「アクション系列」欄には何も記述されていないので、上記処理対象セルのアクション欄は空欄のままとする。（図６、Ｓ２１０）。
【００９８】
次に、もう一つのイベントである「E1[False]」についての抽出レコードの処理について述べる。状態定義レコード表において「E1[False]」についての抽出レコード群は第３行のみであり、その第３行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State2」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「E2[False]」である。よって、状態遷移表における処理対象セルは、「State2」をインデックスとする第４行と、「E2[False]」をインデックスとする左端から第５列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State4」を書き込む。さらに状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクションを上記処理対象セルのアクション欄（セル内下側）に書き込むのであるが、処理対象レコード「アクション系列」欄にはアクションが記述されていないので、上記処理対象セルのアクション欄は空欄のままとする。（図６、Ｓ２１０）。
上記状態定義レコード表、第５行の処理が終了した時点の状態遷移表の状態を図１４に示す。
【００９９】
[状態定義レコード表、第６行の処理]
次に状態遷移表生成部２３はステップＳ２０５に進み、状態定義レコード表の次のレコードを処理対象レコードにする（図６、Ｓ２０５）。本具体例では、図５の状態定義レコード表の最終行である第６行、「アクション実行パス状態」欄のセルが「State5」である状態定義レコードが新たな処理対象レコードに決定される。
【０１００】
次に、状態遷移表生成部２３は、状態定義レコード表の全ての行（レコード）を読み終えたか否かを判定する（図６、Ｓ２０３参照）。本具体例では、状態遷移表生成部２３は全ての行を読み終えていないと判定する（図６、Ｓ２０３、Ｎｏ）。
【０１０１】
次に状態遷移表生成部２３は状態定義レコード表の処理対象レコード「アクション実行パス状態」のセルに記述されている情報が「State0」でないか否かを判定する（図６、Ｓ２０３参照）。本具体例では、処理対象レコードの「アクション実行パス状態」欄の記述は「State5」であるので、ステップＳ２０６に進む。ステップＳ２０６において、状態遷移表生成部２３は処理対象レコードを読む。本具体例では、状態定義レコード表の第３行、「アクション実行パス状態」欄のセルが「State5」である状態定義レコードが読み取られる。
【０１０２】
次に、状態遷移表生成部２３は、処理対象レコードにおける「前イベント」欄に記述されたイベントがあるか否かを判定する（図６、Ｓ２０７）。本具体例では、状態定義レコード表の第６行の「前イベント」欄には、イベント「E2[True]」及び「E2[False]」の記述があるので、ステップＳ２０９へと進む（図６、Ｓ２０７、Ｙｅｓ）。
【０１０３】
状態遷移表生成部２３は、状態定義レコード表から、前イベントに対するアクション実行パス状態を有する状態定義レコード群を抽出する（図６、Ｓ２０９）。本具体例では、状態定義レコード表においてイベント「E2[True]」及び「E2[False]」が「イベント」欄に記述されている状態定義レコードが抽出され、抽出レコード群は「E2[True]」について第４行の状態定義レコードのみ、「E2[False]」について第５行の状態定義レコードのみである。
【０１０４】
次に、状態遷移表生成部２３は、状態遷移表において、抽出レコードの「アクション実行パス状態」欄に記載されたアクション実行パス状態に一致するインデックスを有する行と、処理対象レコードの「イベント」欄に記載されたイベントに一致するインデックスを有する列との交点となる処理対象セルの状態欄に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態を書き込み、同処理対象セルのアクション欄に、処理対象レコードの「アクション系列」欄に記載されたアクションを記述する（図６、Ｓ２１０）。
【０１０５】
状態定義レコード表において「E2[True]」についての抽出レコード群は第４行のみであり、その第４行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State3」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「End」である。よって、状態遷移表における処理対象セルは、「State3」をインデックスとする第５行と、「End」をインデックスとする左端から第６列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State5」を書き込む。さらに状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクションを上記処理対象セルのアクション欄（セル内下側）に書き込むのであるが、処理対象レコード「アクション系列」欄には何も記述されていないので、上記処理対象セルのアクション欄は空欄のままとする。（図６、Ｓ２１０）。
【０１０６】
次に、もう一つのイベントである「E2[False]」についての抽出レコード群の処理について述べる。状態定義レコード表において「E2[False]」についての抽出レコード群は第５行のみであり、その第５行の「アクション実行パス状態」欄に記載されているアクション実行パス状態は「State4」である。また、処理対象レコードの「イベント」欄に記載されたイベントは「End」である。よって、状態遷移表における処理対象セルは、「State4」をインデックスとする第６行と、「End」をインデックスとする左端から第６列との交点であるセルに決定される。状態遷移表生成部２３はこの処理対象セルの状態欄（セル内上側）に、処理対象レコードの「アクション実行パス状態」欄に記載されているアクション実行パス状態「State5」を書き込む。さらに状態遷移表生成部２３は処理対象セルのアクション欄（セル内下側）に、処理対象レコードの「アクション系列」欄に記述されているアクションを上記処理対象セルのアクション欄（セル内下側）に書き込むのであるが、処理対象レコード「アクション系列」欄にはアクションが記述されていないので、上記処理対象セルのアクション欄は空欄のままとする。（図６、Ｓ２１０）。
上記状態定義レコード表、第６行の処理が終了した時点の状態遷移表の状態を図１５に示す。
【０１０７】
［空欄処理］
次に状態遷移表生成部２３はステップＳ２０５に進み、処理対象レコードを次の状態定義レコードとするが、状態定義レコード表は第６行以降の行が無いので、最終行到達と判定する。次に状態遷移表生成部２３はステップＳ２０３に進み、状態定義レコードが終了したか否かを判定する（図６、Ｓ２０３）。ここで、状態遷移表生成部２３は状態定義レコードが終了したと判定し（図６、Ｓ２０３、Ｙｅｓ）、ステップＳ２１１に進む。
【０１０８】
ステップＳ２１１において、状態遷移表生成部２３は状態遷移表の全ての空欄に、該当欄が空欄であることを示す情報として"/"を記述する。該当欄が空欄であることを示す情報が記述された状態の状態遷移表の例を図１６に示す。図１６に示す状態が完成した状態遷移表となる。
以上で、状態遷移表生成処理が終了し、図１６に示した状態遷移表が完成する。
【０１０９】
[実施例1]
次に、本実施の態様の別の実施例について説明する。図１７は、本実施の態様にかかる状態遷移表生成装置に入力される入出力順序系列仕様であるフローチャートを示した図である。このフローチャートは、従業員食堂における代金精算システムの処理内容を示したフローチャートである。
【０１１０】
状態遷移表生成装置は、図１７のフローチャートを読み取ると、まず、状態定義レコード表生成処理（図３参照）を実行する。
図１７のフローチャートはステップＳ３０１からステップＳ３１２までの１２ステップで構成され、そのうち条件分岐はステップＳ３０３，ステップＳ３０５，ステップＳ３０８である。
【０１１１】
状態遷移表生成装置、より詳しくは状態定義レコード表生成部は図１７のフローチャートの各処理、Ｓ３０１、Ｓ３０２、Ｓ３０４、Ｓ３０６、Ｓ３０７、Ｓ３０９、Ｓ３１０、Ｓ３１１、Ｓ３１２にアクションとしてラベル付けを行い、Ａ１，Ａ２、Ａ４，Ａ５，Ａ６，Ａ８，Ａ９，Ａ３，Ａ７とする。また、状態遷移表生成装置、より詳しくは状態定義レコード表生成部は、図１７のフローチャートの各条件分岐Ｓ３０３、Ｓ３０５、Ｓ３０８のTrue（Ｙｅｓ側分岐に対応する）、False（Ｎｏ側分岐に対応する）をイベントとしてラベル付けを行い、それぞれをＥ１[True]（Ｓ３０３、Ｙｅｓ）及びＥ１[False]（Ｓ３０３、Ｎｏ）、Ｅ２[True]（Ｓ３０５、Ｙｅｓ）及びＥ２[False]（Ｓ３０５、Ｎｏ）、Ｅ３[True]（Ｓ３０８、Ｙｅｓ）及びＥ３[False]（Ｓ３０８、Ｎｏ）とする。
【０１１２】
状態遷移表生成装置１１、より詳しくは状態定義レコード表生成部２２は状態定義レコード表生成処理（図３参照）を続行することにより、図１８に示す状態定義レコード表を生成する。図１８は、状態定義レコード表生成処理を実行することによって、図１７のフローチャートから生成された状態定義レコード表の一例を示す図である。
【０１１３】
状態遷移表生成装置１１、より詳しくは状態遷移表生成部２３は図１８に示す状態定義レコード表を受信すると、これに基づいて状態遷移表生成処理（図６参照）を実行し、状態遷移表を生成し出力する。図１９は、状態遷移表生成処理によって図１８の状態定義レコードから生成された状態遷移表の例を示す。
【０１１４】
［実施例１：追加機能］
状態遷移表生成装置１１、より詳しくはイベント／アクション定義レコード生成部２４は、各イベント並びにアクションに付したラベルと、各イベント並びにアクションの内容を対応付けして示した表である、「イベント/アクション定義レコード」を生成する。
図２０は、図１８に示したフローチャートから状態遷移表を生成する際に、状態遷移表生成装置、より詳しくは状態定義レコード表生成部によって生成される「イベント/アクション定義レコード」の一例を示した図である。
【０１１５】
かかる「イベント/アクション定義レコード」を生成し、利用することによりユーザは状態遷移表の内容検証、検討などをより容易に行えるようになる。例えば、生成された状態遷移表を画面上に表示させた状態で、状態遷移表内のラベル（Ａ１、など）の上にカーソルやポインタを置くと、「イベント/アクション定義レコード」が参照され、ポップアップウインドウが開いてその中に当該ラベルに対応する「意味」が表示されるような機能を実現することも可能となる。
【０１１６】
［実施例２］
上述した例では、状態遷移表生成装置１１の入力である入出力順序系列仕様としてフローチャートを利用する態様を説明したが、状態遷移表生成装置１１が利用可能な入出力順序系列仕様は、フローチャートに限られず、例えば、プログラムのソースコードであってもかまわない。以下に、プログラムのソースコードを入出力順序系列仕様として扱う場合の状態遷移表生成装置１１の動作例を説明する。
【０１１７】
まず、状態遷移表生成装置１１はソースコードに基づいて状態定義レコード表を生成する。これは図３に示した状態定義レコード生成処理を実行することによって行われる。但し、ｉｆ文、ｗｈｉｌｅ文が「条件分岐」として扱われ、その他の命令文は「処理」として扱われる。
状態遷移表生成装置１１は、生成した状態定義レコード表に基づいて状態遷移表を生成する。この処理は図６に示す状態遷移表生成処理によって行われる。
【０１１８】
図２１は、状態遷移表生成装置１１の入力となるソースコードの一例を示す図である。図２２は、図２１のソースコードにイベント及びアクションのラベルが付された状態を示す図である。図２２に示したようにイベント及びアクションのラベルを付し、状態定義レコード表生成処理（図３参照）を実行した結果得られる状態定義レコード表の例を図２３に示す。図２３に示した状態定義レコード表に基づいて、状態遷移表生成処理（図６参照）を実行した結果得られる状態遷移表の例を図２４に示す。すなわち、状態遷移表生成装置１１は、図２１に示したソースコードから図２４に示す状態遷移表を生成することが可能である。
【０１１９】
［まとめ］
本実施の態様によれば、状態遷移表等の事象-応答型の仕様を入力情報として検査コードを自動変換するモデル検査支援ツールに対して、フローチャート等の時系列の入力情報を扱うことができるようになる。
本実施の態様によれば、時系列の仕様の条件と処理を、状態遷移のイベント、条件、アクションに適切に対応させることで、状態遷移系に変換させても、条件に応じた処理のパスを理解容易にすることができる。
【０１２０】
[第２の実施の形態]
次に、第２の実施の形態について説明する。第２の実施の形態は、条件分岐と処理にイベントとアクションのラベル付けを行う処理が、第１の実施の形態と異なる。より具体的には、第１の実施の形態では、イベントとアクションの組み合わせをアクション実行パス状態として定義するのに対して、第２の実施の形態ではイベントをアクション実行パスとする点で異なっている。
【０１２１】
[装置の構成例]
第２の実施の形態にかかる状態遷移表生成装置１１Ａの構成例を図２５に示す。状態遷移表生成装置１１Ａは、第１の実施の形態にかかる状態遷移表生成装置１１の構成と基本的に同様であるが、状態定義レコード生成部２２に代えて、状態定義レコード生成部２２Ａを有する点で異なっている。他の構成要素については同一の構成要素には同一の参照番号を付し、これら構成要素の詳細な説明は省略する。
【０１２２】
[動作例]
次に、状態遷移表生成装置１１Ａの動作例を説明する。入出力順序系列仕様記憶部２１、状態遷移表生成部２３、イベント／アクション定義レコード生成部２４のそれぞれは、第１の実施の形態における動作と同様なので、これらの動作の説明は省略する。以下に、状態定義レコード生成部２２Ａの動作を述べる。
【０１２３】
図２６と図２７は、状態定義レコード生成部２２Ａの動作である状態定義レコード生成処理の一例を示すフローチャートであって、図２７は、図２６に続くフローチャートである。
図２６と図２７に示す状態定義レコード生成部２２Ａの動作である状態定義レコード生成処理は、図３Ａ，図３Ｂに示す状態定義レコード生成部２２の動作と基本的に同じ処理内容であるが、ステップＳ９０Ａにおいて異なっている。
【０１２４】
ステップＳ９０Ａにおいて、状態定義レコード生成部２２Ａは同一の状態名（アクション実行パス状態を特定する情報）を有する状態定義レコードを２つ作成し、一方のレコードに当該条件分岐の「True」をそのイベント欄に登録し、他方のレコードのイベント欄に「False」を登録する。
【０１２５】
その他の各ステップについては、第１の実施の形態にかかる図３Ａ、図３Ｂに示したステップと同様なので、同一の処理内容を有するステップには同一の参照番号を付し、これらの詳細な説明は省略する。
【０１２６】
第２の実施の形態における状態定義レコード生成処理によって状態定義レコードが生成される。この状態定義レコードから第１の実施の形態の状態遷移表生成処理（図６参照）と同様の処理によって、状態遷移表が生成されることになる。
【０１２７】
第２の実施の形態において生成される状態遷移表は、第２の実施の形態のそれに比べて、アクション実行パス状態（状態定義レコード）の数を少なくすることができ、その結果最終的生成される状態遷移表もより簡素化されたものを生成することができ、ユーザの状態遷移表の使用の際の負担を軽減できる。
【０１２８】
[具体例その１]
第２の実施の形態にかかる状態遷移表生成装置１１Ａの動作例の具体例を述べる。図２８は、本具体例において上記状態定義レコード表の元となる入出力順序系列仕様１０であるフローチャート（「処理対象フローチャート」と呼ぶ）である。図２８は、前述した図４に示すフローチャートと同様であるので、このフローチャートの内容の説明は省略する。図２９は、図２８の処理対象フローチャートから生成された状態定義レコード表の例を示した図である。
【０１２９】
まず、状態定義レコード表生成部２２Ａは、図２８に示したフローチャートの条件分岐、処理の各要素にそれぞれイベントとアクションの番号付けをする（図２６、Ｓ１０）。具体的には、第1の条件分岐Ｓ１０１にはイベント番号「Ｅ１」を付与し、第２の条件分岐Ｓ１０４にはイベント番号「Ｅ２」を付与する。また、アクションＳ１０２、Ｓ１０３、Ｓ１０４にはそれぞれアクション番号「Ａ１」、「Ａ２」、「Ａ３」を付与する。
【０１３０】
次に、状態定義レコード表生成部２２は、状態定義レコード表を生成し、フローチャートの最初の要素である「Start」を読み取ると、アクション実行パス状態欄に「State0」を格納し、且つそのイベント欄にイベント名「Start」と格納したレコードを状態定義レコード表に加える（図２６、Ｓ２０）。
【０１３１】
次に、状態定義レコード表生成部２２Ａは、「終了（End）」以外の全ての要素を読み込み済みか否かを判定する（図２６、Ｓ３０）。この具体例では、全ての要素を読み込んでいないので、判定は「Ｎｏ」となりステップＳ４０に移行する。
【０１３２】
次に、状態定義レコード表生成部２２Ａは、ステップＳ３０の判定後、処理対象フローチャートの連結部分から次の一要素を読み取る（図２６、Ｓ４０）。この例では処理対象フローチャートの要素「Ｅ１」を読み込む。
【０１３３】
次に、状態定義レコード表生成部２２は、読み取った要素が条件分岐か否かを判定する（図２６、Ｓ５０）。この例では要素「Ｅ１」は条件分岐であると判定される（図２６、Ｓ５０、Ｙｅｓ）。
【０１３４】
次に、状態定義レコード表生成部２２Ａは、当該条件分岐によって生じる状態を定義する状態名を決定する（図２６、Ｓ７０）。この例では、状態定義レコード表生成部２２は、条件分岐「Ｅ１」を状態名「State1」と定める。
【０１３５】
次に、状態定義レコード表生成部２２Ａは、その条件分岐がイベントとして状態定義レコード表に登録済みであるか否かを判定する（図２６、Ｓ８０）。この例では、条件分岐「Ｅ１」は未だ状態定義レコード表に登録済みではないと判定し（図２６、Ｓ８０、Ｎｏ）、ステップＳ９０Ａに移行する。
【０１３６】
ステップＳ９０Ａにおいて、状態定義レコード表生成部２２Ａは、状態定義レコード表に新たに状態定義レコードを２つ作成し、一方のレコードのイベント欄にその条件分岐の「True」を登録し、他方のレコードのイベント欄にその条件分岐の「False」を登録する。この例では、状態定義レコード表生成部２２Ａは、図２９の状態定義レコード表において、第２行と第３行を作成し、第２行の「アクション実行パス状態」欄に状態名「State1」を記述するとともに「イベント」欄に「E1[True]」を記述する。またさらに状態定義レコード表生成部２２は、第３行の「アクション実行パス状態」欄に状態名「State1」と記述するとともに「イベント」欄に「E1[False]」を記述する。
【０１３７】
次に、状態定義レコード表生成部２２Ａは、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（図２６、Ｓ１００）。この例では、状態定義レコード表生成部２２Ａは、直前に登録したイベントである「E1[True]」（第２行）、「E1[False]」（第３行）に対応する「前イベント」欄に、直前に状態を定義したレコード（第１行）の「イベント」欄に記述されたイベント「Start」を記述する。
【０１３８】
次に、状態定義レコード表生成部２２Ａは、ステップＳ３０に戻りその後ステップＳ４０において、要素「Ｅ１」の次の要素「Ａ１」を読み取る（図２６、Ｓ４０）。
次に、状態定義レコード表生成部２２Ａは、読み取った要素が条件分岐か否かを判定する。この例では要素「Ａ１」は条件分岐ではないと判定される（図２６、Ｓ５０、Ｎｏ）。
【０１３９】
次に、状態定義レコード表生成部２２Ａは、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号を状態定義レコード表に登録する（図２６、Ｓ６０）。具体的には、図２９に示した状態定義レコード表の第２行の「アクション系列」欄に「Ａ１」と記述する。
【０１４０】
次に、状態定義レコード表生成部２２Ａは、ステップＳ３０に戻り、続くステップＳ４０において、要素「Ａ１」の次の要素「Ａ２」を読み取る（図２６、Ｓ４０）。
【０１４１】
次に、状態定義レコード表生成部２２Ａは、読み取った要素が条件分岐か否かを判定する（図２６、Ｓ５０）。この例では要素「Ａ２」は条件分岐ではないと判定される（図２６、Ｓ５０、Ｎｏ）。
【０１４２】
次に、状態定義レコード表生成部２２Ａは、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号を状態定義レコード表に登録する（図２６、Ｓ６０）。具体的には、図２９に示した状態定義レコード表の第２行の「アクション系列」欄に「Ａ２」を追加して記述する。
【０１４３】
次に、状態定義レコード表生成部２２Ａは、ステップＳ３０に戻りその後ステップＳ４０において、処理対象フローチャートにおける要素「Ａ２」の次の要素「Ｅ２」を読み取る（図２６、Ｓ４０）。
【０１４４】
次に、状態定義レコード表生成部２２Ａは、読み取った要素が条件分岐か否かを判定する（図２６、Ｓ５０）。この例では要素「Ｅ２」は条件分岐であると判定される（図２６、Ｓ５０、Ｙｅｓ）。
【０１４５】
次に、状態定義レコード表生成部２２Ａは、当該条件分岐によって生じる状態を定義する状態名を決定する（図２６、Ｓ７０）。この例では、状態定義レコード表生成部２２Ａは、条件分岐「Ｅ２」を状態名「State2」と定める。
【０１４６】
次に、状態定義レコード表生成部２２Ａは、その条件分岐がイベントとして状態定義レコード表に登録済みであるか否かを判定する（図２６、Ｓ８０）。この例では、条件分岐「Ｅ２」は未だ状態定義レコード表に登録済みではないと判定し（図２６、Ｓ８０、Ｎｏ）、ステップＳ９０Ａに移行する。
【０１４７】
ステップＳ９０Ａにおいて、状態定義レコード表生成部２２Ａは、状態定義レコード表に新たに状態定義レコードを２つ追加し、その条件分岐の「True」を一方のレコードのイベント欄に登録し、他方のレコードにその条件分岐の「False」を登録する。この例では、状態定義レコード表生成部２２は、図２９に示す状態定義レコード表に第４行と第５行を作成し、第４行の「アクション実行パス状態」欄に「State2」を記述するとともにその「イベント」欄に「E2[True]」を記述する。またさらに状態定義レコード表生成部２２Ａは、第５行の「アクション実行パス状態」欄に「State2」と記述するとともにその「イベント」欄に「E2[False]」を記述する。
【０１４８】
次に、状態定義レコード表生成部２２Ａは、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（図２６、Ｓ１００)。この例では、状態定義レコード表生成部２２Ａは、第４行及び第５行の登録の直前に登録したレコード（第２行、第3行のレコード）のイベント欄に記述された「E1[True]」（第２行）及び「E1[False]」（第３行）を第４行、第５行の「前イベント」欄に記述する。
【０１４９】
次に、状態定義レコード表生成部２２Ａは、ステップＳ３０に戻りその後ステップＳ４０において、要素「Ｅ２」の次の要素「Ａ３」を読み取る（図２６、Ｓ４０）。
次に、状態定義レコード表生成部２２Ａは、読み取った要素が条件分岐か否かを判定する（図２６、Ｓ５０）。この例では要素「Ａ３」は条件分岐ではないと判定される（図２６、Ｓ５０、Ｎｏ）。
【０１５０】
次に、状態定義レコード表生成部２２Ａは、その要素（処理）を当該条件のイベントに対するアクションとして、読み取った要素の要素番号を状態定義レコード表に登録する（図２６、Ｓ６０）。具体的には、図２９に示した状態定義レコード表の第４行の「アクション系列」欄に「Ａ３」を記述する。
【０１５１】
次に、状態定義レコード表生成部２２Ａは、ステップＳ３０に戻り、終了（Ｅｎｄ）以外の全ての要素を読み込み済みか否かを判定する（図２６、Ｓ３０）。この例では、状態定義レコード表生成部２２Ａは、終了（Ｅｎｄ）以外の全ての要素を読み込み済みであると判定し（Ｓ３０、Ｙｅｓ）、図２７のステップＳ１１０に進む。
【０１５２】
ステップＳ１１０において、状態定義レコード表生成部２２Ａは現在の状態数を含む状態名をアクション実行パス状態欄に格納し、且つイベント欄に「End」を格納した新たな状態定義レコードを生成し、状態定義レコード表に追加する（図２７、Ｓ１１０）。図２９の例では、第６行のレコードに相当する。
【０１５３】
次に、状態定義レコード表生成部２２Ａは、登録した或いは登録済みイベントの前イベントに、前記２つのレコードの直前に状態を定義したレコードのイベントを登録する（図２７、Ｓ１２０)。この例では、状態定義レコード表生成部２２Ａは、第６行の登録の直前に登録したレコード（第４行、第５行に相当するレコード）のイベント欄に記述された「E2[True]」（第４行）及び「E2[False]」（第５行）を第６行の「前イベント」欄に記述する。
以上で、図２６に示したフローチャートの処理に基づいて、図２９に示した状態定義レコード表が完成する。
【０１５４】
[状態遷移表の生成]
次に、状態遷移表生成装置１１Ａ、より詳しくは状態遷移表生成部２３は、図２９に示した状態定義レコード表のデータを受信して、このデータを用いて、状態遷移表生成処理(図６参照)を実行し状態遷移表を生成する。状態遷移表生成処理の内容は第１の実施の形態と同様である。
図３０に、図２９に示した状態定義レコード表のデータから生成された状態遷移表の例を示す。
【０１５５】
[実施例その２]
第２の実施の形態にかかる状態遷移表生成装置１１Ａの動作例の別の具体例を述べる。図３１に示すＩＰアドレスの割り当て処理を状態遷移表生成装置１１Ａを用いて状態遷移表を生成する例を示す。
【０１５６】
図３１は、ＰＣ−１、ＰＣ−２、ＰＣ−３、ＰＣ−４からなるネットワークにおいて、ＩＰアドレスの割り当てを行う処理の例を示したシーケンス図である。ＰＣ−３、ＰＣ−４はともにＤＨＣＰサーバとして機能する。
【０１５７】
まず、ＰＣ−１が起動時にＩＰアドレスの有無を判定し、ＩＰアドレスが割り当てられていない場合には、ネットワーク内の他の装置にＤＩＳＣＯＶＥＲメッセージをブロードキャストする（Ｓ３１０１、Ｓ３１０２、Ｓ３１０３）。
【０１５８】
ＤＩＳＣＯＶＥＲメッセージを受信したＤＨＣＰサーバであるＰＣ−３、ＰＣ−４は、割り当てる候補となるＩＰアドレスが含まれているＯＦＦＥＲメッセージを送信する（Ｓ３１０４、Ｓ３１０５）。この例では、ＰＣ−３はＩＰ１というＩＰアドレスを提示し、ＰＣ−４はＩＰ２というＩＰアドレスを提示したものとする。
【０１５９】
ＰＣ−３，ＰＣ−４のそれぞれからＯＦＦＥＲメッセージを受信したクライアントであるＰＣ−1は、提示されたＩＰアドレスに問題がなければ、正式にサーバにIPを要求するＲＥＱＵＥＳＴメッセージを送信する（Ｓ３１０６、Ｓ３１０７）。この例では、ＰＣ−１はＩＰ１を選択して、ＲＥＱＵＥＳＴメッセージを送信した者とする。
【０１６０】
ＩＰ１についてのＲＥＱＵＥＳＴメッセージを受信したＰＣ−３は自分が選択されたことを同じユーザーIPアドレスが返送されたことで確認して、問題なければ「PACK」パケットを返信し、問題あれば「PNAK」パケットを返信する（Ｓ３１０８）。
【０１６１】
PACKを正常に受信したPC-1は、OFFERで指定されたユーザIPアドレスを自分のIPアドレスとして保存し、以降はこのIPアドレスで通信を行うように内部設定する。一方、「PNAK」が返信された時は、再度DISCOVERの送信を実行する（Ｓ３１０９）。
【０１６２】
この実施の例では、上記のシーケンス図に示される処理のうち、クライアントであるＰＣ−１の処理フローチャートと、ＤＨＣＰサーバであるＰＣ−３の処理フローチャートを、それぞれ入出力順序系列仕様１０として用意し、それぞれの入出力順序系列仕様１０から状態遷移表生成装置１１Ａに状態遷移表を生成させる。
【０１６３】
[クライアント側]
図３２は、クライアントであるＰＣ−１の処理フローチャートの例を示す図である。このフローチャートに対応するデータ等を入出力順序系列仕様１０から状態遷移表生成装置１１Ａに入力する。図３３は、状態名（アクション実行パス状態）が付された図３２のフローチャートを示す。図３４は、図３２のフローチャート（入出力順序系列仕様１０）から状態遷移表生成装置１１Ａが生成した状態遷移表を状態遷移図に示した図である。
【０１６４】
[ＤＨＣＰサーバ側]
図３５は、ＤＨＣＰサーバであるＰＣ−３の処理フローチャートの例を示す図である。このフローチャートに対応するデータ等を入出力順序系列仕様１０から状態遷移表生成装置１１Ａに入力する。図３６は、状態名（アクション実行パス状態）が付された図３５のフローチャートを示す。分岐条件Ｅ１，Ｅ２，Ｅ３，Ｅ４について、それぞれ状態名（アクション実行パス状態）State1,  State2,  State3,  State4が付与され、これら状態名ごとに状態定義レコード表のレコードが生成されることとなる。図３７は、図３５のフローチャート（入出力順序系列仕様１０）から状態遷移表生成装置１１Ａが生成した状態遷移表を状態遷移図に示した図である。
【０１６５】
なお、本実施の形態の変形として、条件分岐が連続している場合（図３６、Ｅ２〜Ｅ３）は、これを一つの条件分岐として扱い、一つの状態として状態遷移表の生成を行うようにしてもよい。この例に上記変形を適用すると、条件分岐であるＥ２〜Ｅ４は、一つの状態「Ｓｔａｔｅ２」として処理される。
【０１６６】
[その他] 
以上、本発明の実施の形態を説明したが、本発明はこれらに限定されるものではなく、発明の趣旨を逸脱しない範囲内において、種々の変更、追加、組み合わせ等が可能である。
変形例として、状態遷移表生成装置１１は、状態定義レコード生成部２２と状態定義レコード生成部２２Ａとをともに有しており、ユーザの指定により一方を選択して、状態定義レコード表の生成、それに基づく状態遷移表の生成を行わせるように変形することもできる。
【符号の説明】
【０１６７】
１０・・・入出力順序系列仕様；  １１・・・状態遷移表生成装置；  １２・・・状態遷移表；  ２１・・・入出力順序系列仕様記憶部；  ２２、２２Ａ・・・状態定義レコード生成部；  ２３・・・状態遷移表生成部；  ２４・・・イベント／アクション定義レコード生成部
【図１】
0005774468.tif 000002
【図２】
0005774468.tif 000003
【図３Ａ】
0005774468.tif 000004
【図３Ｂ】
0005774468.tif 000005
【図４】
0005774468.tif 000006
【図５】
0005774468.tif 000007
【図６】
0005774468.tif 000008
【図７】
0005774468.tif 000009
【図８】
0005774468.tif 000010
【図９】
0005774468.tif 000011
【図１０】
0005774468.tif 000012
【図１１】
0005774468.tif 000013
【図１２】
0005774468.tif 000014
【図１３】
0005774468.tif 000015
【図１４】
0005774468.tif 000016
【図１５】
0005774468.tif 000017
【図１６】
0005774468.tif 000018
【図１７】
0005774468.tif 000019
【図１８】
0005774468.tif 000020
【図１９】
0005774468.tif 000021
【図２０】
0005774468.tif 000022
【図２１】
0005774468.tif 000023
【図２２】
0005774468.tif 000024
【図２３】
0005774468.tif 000025
【図２４】
0005774468.tif 000026
【図２５】
0005774468.tif 000027
【図２６】
0005774468.tif 000028
【図２７】
0005774468.tif 000029
【図２８】
0005774468.tif 000030
【図２９】
0005774468.tif 000031
【図３０】
0005774468.tif 000032
【図３１】
0005774468.tif 000033
【図３２】
0005774468.tif 000034
【図３３】
0005774468.tif 000035
【図３４】
0005774468.tif 000036
【図３５】
0005774468.tif 000037
【図３６】
0005774468.tif 000038
【図３７】
0005774468.tif 000039