rustate

Struct ModelChecker

Source 
pub struct ModelChecker<'a> { /* private fields */ }
Expand description

モデルチェッカー

Implementations§

Source§

impl<'a> ModelChecker<'a>

Source

pub fn new(machine: &'a Machine) -> Self

新しいモデルチェッカーを作成

Examples found in repository?
examples/model_based_testing.rs (line 65)
6fn main() {
7    // 状態マシンを作成
8    let machine = create_test_machine();
9    println!("状態マシンを作成しました: {}", machine.name);
10
11    // テストケース生成
12    println!("\n=== テストケースの生成 ===");
13    let mut generator = TestGenerator::new(&machine);
14
15    println!("\n>> 全状態カバレッジのテストケース");
16    let state_tests = generator.generate_all_states();
17    for test in &state_tests {
18        println!(
19            "- {}: {} -> {} (イベント数: {})",
20            test.name,
21            test.initial_state,
22            test.expected_state,
23            test.events.len()
24        );
25    }
26
27    println!("\n>> 全遷移カバレッジのテストケース");
28    let transition_tests = generator.generate_all_transitions();
29    for test in &transition_tests {
30        println!(
31            "- {}: {} -> {} (イベント数: {})",
32            test.name,
33            test.initial_state,
34            test.expected_state,
35            test.events.len()
36        );
37    }
38
39    println!("\n>> ループカバレッジのテストケース");
40    let loop_tests = generator.generate_loop_coverage();
41    for test in &loop_tests {
42        println!(
43            "- {}: {} -> {} (イベント数: {})",
44            test.name,
45            test.initial_state,
46            test.expected_state,
47            test.events.len()
48        );
49    }
50
51    // テスト実行
52    println!("\n=== テスト実行 ===");
53    let mut runner = TestRunner::new(&machine);
54
55    println!("\n>> 状態カバレッジテストの実行");
56    let state_results = runner.run_tests(state_tests);
57    print_test_results(&state_results);
58
59    println!("\n>> 遷移カバレッジテストの実行");
60    let transition_results = runner.run_tests(transition_tests);
61    print_test_results(&transition_results);
62
63    // モデル検査
64    println!("\n=== モデル検査 ===");
65    let mut checker = ModelChecker::new(&machine);
66
67    // 到達可能性プロパティ
68    let reachability = Property {
69        name: "赤信号に到達可能か".to_string(),
70        property_type: PropertyType::Reachability,
71        target_states: vec!["red".to_string()],
72        description: Some("赤信号状態に到達できることを確認".to_string()),
73    };
74
75    let result = checker.verify_property(&reachability);
76    println!("\n>> プロパティ: {}", reachability.name);
77    println!(
78        "結果: {}",
79        if result.satisfied {
80            "満たされています"
81        } else {
82            "満たされていません"
83        }
84    );
85    if let Some(msg) = result.message {
86        println!("メッセージ: {}", msg);
87    }
88
89    // 安全性プロパティ
90    let safety = Property {
91        name: "存在しない状態に到達しないか".to_string(),
92        property_type: PropertyType::Safety,
93        target_states: vec!["invalid".to_string()],
94        description: Some("存在しない状態に決して到達しないことを確認".to_string()),
95    };
96
97    let result = checker.verify_property(&safety);
98    println!("\n>> プロパティ: {}", safety.name);
99    println!(
100        "結果: {}",
101        if result.satisfied {
102            "満たされています"
103        } else {
104            "満たされていません"
105        }
106    );
107    if let Some(msg) = result.message {
108        println!("メッセージ: {}", msg);
109    }
110
111    // デッドロックの検出
112    println!("\n>> デッドロック検出");
113    let deadlocks = checker.detect_deadlocks();
114    if deadlocks.is_empty() {
115        println!("デッドロック状態はありません");
116    } else {
117        println!("デッドロック状態: {}", deadlocks.join(", "));
118    }
119
120    // 到達不可能な状態の検出
121    println!("\n>> 到達不可能な状態の検出");
122    let unreachable = checker.detect_unreachable_states();
123    if unreachable.is_empty() {
124        println!("到達不可能な状態はありません");
125    } else {
126        println!("到達不可能な状態: {}", unreachable.join(", "));
127    }
128}
Source

pub fn verify_property(&mut self, property: &Property) -> VerificationResult

プロパティを検証

Examples found in repository?
examples/model_based_testing.rs (line 75)
6fn main() {
7    // 状態マシンを作成
8    let machine = create_test_machine();
9    println!("状態マシンを作成しました: {}", machine.name);
10
11    // テストケース生成
12    println!("\n=== テストケースの生成 ===");
13    let mut generator = TestGenerator::new(&machine);
14
15    println!("\n>> 全状態カバレッジのテストケース");
16    let state_tests = generator.generate_all_states();
17    for test in &state_tests {
18        println!(
19            "- {}: {} -> {} (イベント数: {})",
20            test.name,
21            test.initial_state,
22            test.expected_state,
23            test.events.len()
24        );
25    }
26
27    println!("\n>> 全遷移カバレッジのテストケース");
28    let transition_tests = generator.generate_all_transitions();
29    for test in &transition_tests {
30        println!(
31            "- {}: {} -> {} (イベント数: {})",
32            test.name,
33            test.initial_state,
34            test.expected_state,
35            test.events.len()
36        );
37    }
38
39    println!("\n>> ループカバレッジのテストケース");
40    let loop_tests = generator.generate_loop_coverage();
41    for test in &loop_tests {
42        println!(
43            "- {}: {} -> {} (イベント数: {})",
44            test.name,
45            test.initial_state,
46            test.expected_state,
47            test.events.len()
48        );
49    }
50
51    // テスト実行
52    println!("\n=== テスト実行 ===");
53    let mut runner = TestRunner::new(&machine);
54
55    println!("\n>> 状態カバレッジテストの実行");
56    let state_results = runner.run_tests(state_tests);
57    print_test_results(&state_results);
58
59    println!("\n>> 遷移カバレッジテストの実行");
60    let transition_results = runner.run_tests(transition_tests);
61    print_test_results(&transition_results);
62
63    // モデル検査
64    println!("\n=== モデル検査 ===");
65    let mut checker = ModelChecker::new(&machine);
66
67    // 到達可能性プロパティ
68    let reachability = Property {
69        name: "赤信号に到達可能か".to_string(),
70        property_type: PropertyType::Reachability,
71        target_states: vec!["red".to_string()],
72        description: Some("赤信号状態に到達できることを確認".to_string()),
73    };
74
75    let result = checker.verify_property(&reachability);
76    println!("\n>> プロパティ: {}", reachability.name);
77    println!(
78        "結果: {}",
79        if result.satisfied {
80            "満たされています"
81        } else {
82            "満たされていません"
83        }
84    );
85    if let Some(msg) = result.message {
86        println!("メッセージ: {}", msg);
87    }
88
89    // 安全性プロパティ
90    let safety = Property {
91        name: "存在しない状態に到達しないか".to_string(),
92        property_type: PropertyType::Safety,
93        target_states: vec!["invalid".to_string()],
94        description: Some("存在しない状態に決して到達しないことを確認".to_string()),
95    };
96
97    let result = checker.verify_property(&safety);
98    println!("\n>> プロパティ: {}", safety.name);
99    println!(
100        "結果: {}",
101        if result.satisfied {
102            "満たされています"
103        } else {
104            "満たされていません"
105        }
106    );
107    if let Some(msg) = result.message {
108        println!("メッセージ: {}", msg);
109    }
110
111    // デッドロックの検出
112    println!("\n>> デッドロック検出");
113    let deadlocks = checker.detect_deadlocks();
114    if deadlocks.is_empty() {
115        println!("デッドロック状態はありません");
116    } else {
117        println!("デッドロック状態: {}", deadlocks.join(", "));
118    }
119
120    // 到達不可能な状態の検出
121    println!("\n>> 到達不可能な状態の検出");
122    let unreachable = checker.detect_unreachable_states();
123    if unreachable.is_empty() {
124        println!("到達不可能な状態はありません");
125    } else {
126        println!("到達不可能な状態: {}", unreachable.join(", "));
127    }
128}
Source

pub fn get_reachable_states(&mut self) -> HashSet<String>

すべてのリーチャブルな状態を取得

Source

pub fn detect_deadlocks(&mut self) -> Vec<String>

デッドロック状態を検出

Examples found in repository?
examples/model_based_testing.rs (line 113)
6fn main() {
7    // 状態マシンを作成
8    let machine = create_test_machine();
9    println!("状態マシンを作成しました: {}", machine.name);
10
11    // テストケース生成
12    println!("\n=== テストケースの生成 ===");
13    let mut generator = TestGenerator::new(&machine);
14
15    println!("\n>> 全状態カバレッジのテストケース");
16    let state_tests = generator.generate_all_states();
17    for test in &state_tests {
18        println!(
19            "- {}: {} -> {} (イベント数: {})",
20            test.name,
21            test.initial_state,
22            test.expected_state,
23            test.events.len()
24        );
25    }
26
27    println!("\n>> 全遷移カバレッジのテストケース");
28    let transition_tests = generator.generate_all_transitions();
29    for test in &transition_tests {
30        println!(
31            "- {}: {} -> {} (イベント数: {})",
32            test.name,
33            test.initial_state,
34            test.expected_state,
35            test.events.len()
36        );
37    }
38
39    println!("\n>> ループカバレッジのテストケース");
40    let loop_tests = generator.generate_loop_coverage();
41    for test in &loop_tests {
42        println!(
43            "- {}: {} -> {} (イベント数: {})",
44            test.name,
45            test.initial_state,
46            test.expected_state,
47            test.events.len()
48        );
49    }
50
51    // テスト実行
52    println!("\n=== テスト実行 ===");
53    let mut runner = TestRunner::new(&machine);
54
55    println!("\n>> 状態カバレッジテストの実行");
56    let state_results = runner.run_tests(state_tests);
57    print_test_results(&state_results);
58
59    println!("\n>> 遷移カバレッジテストの実行");
60    let transition_results = runner.run_tests(transition_tests);
61    print_test_results(&transition_results);
62
63    // モデル検査
64    println!("\n=== モデル検査 ===");
65    let mut checker = ModelChecker::new(&machine);
66
67    // 到達可能性プロパティ
68    let reachability = Property {
69        name: "赤信号に到達可能か".to_string(),
70        property_type: PropertyType::Reachability,
71        target_states: vec!["red".to_string()],
72        description: Some("赤信号状態に到達できることを確認".to_string()),
73    };
74
75    let result = checker.verify_property(&reachability);
76    println!("\n>> プロパティ: {}", reachability.name);
77    println!(
78        "結果: {}",
79        if result.satisfied {
80            "満たされています"
81        } else {
82            "満たされていません"
83        }
84    );
85    if let Some(msg) = result.message {
86        println!("メッセージ: {}", msg);
87    }
88
89    // 安全性プロパティ
90    let safety = Property {
91        name: "存在しない状態に到達しないか".to_string(),
92        property_type: PropertyType::Safety,
93        target_states: vec!["invalid".to_string()],
94        description: Some("存在しない状態に決して到達しないことを確認".to_string()),
95    };
96
97    let result = checker.verify_property(&safety);
98    println!("\n>> プロパティ: {}", safety.name);
99    println!(
100        "結果: {}",
101        if result.satisfied {
102            "満たされています"
103        } else {
104            "満たされていません"
105        }
106    );
107    if let Some(msg) = result.message {
108        println!("メッセージ: {}", msg);
109    }
110
111    // デッドロックの検出
112    println!("\n>> デッドロック検出");
113    let deadlocks = checker.detect_deadlocks();
114    if deadlocks.is_empty() {
115        println!("デッドロック状態はありません");
116    } else {
117        println!("デッドロック状態: {}", deadlocks.join(", "));
118    }
119
120    // 到達不可能な状態の検出
121    println!("\n>> 到達不可能な状態の検出");
122    let unreachable = checker.detect_unreachable_states();
123    if unreachable.is_empty() {
124        println!("到達不可能な状態はありません");
125    } else {
126        println!("到達不可能な状態: {}", unreachable.join(", "));
127    }
128}
Source

pub fn detect_unreachable_states(&mut self) -> Vec<String>

到達不可能な状態を検出

Examples found in repository?
examples/model_based_testing.rs (line 122)
6fn main() {
7    // 状態マシンを作成
8    let machine = create_test_machine();
9    println!("状態マシンを作成しました: {}", machine.name);
10
11    // テストケース生成
12    println!("\n=== テストケースの生成 ===");
13    let mut generator = TestGenerator::new(&machine);
14
15    println!("\n>> 全状態カバレッジのテストケース");
16    let state_tests = generator.generate_all_states();
17    for test in &state_tests {
18        println!(
19            "- {}: {} -> {} (イベント数: {})",
20            test.name,
21            test.initial_state,
22            test.expected_state,
23            test.events.len()
24        );
25    }
26
27    println!("\n>> 全遷移カバレッジのテストケース");
28    let transition_tests = generator.generate_all_transitions();
29    for test in &transition_tests {
30        println!(
31            "- {}: {} -> {} (イベント数: {})",
32            test.name,
33            test.initial_state,
34            test.expected_state,
35            test.events.len()
36        );
37    }
38
39    println!("\n>> ループカバレッジのテストケース");
40    let loop_tests = generator.generate_loop_coverage();
41    for test in &loop_tests {
42        println!(
43            "- {}: {} -> {} (イベント数: {})",
44            test.name,
45            test.initial_state,
46            test.expected_state,
47            test.events.len()
48        );
49    }
50
51    // テスト実行
52    println!("\n=== テスト実行 ===");
53    let mut runner = TestRunner::new(&machine);
54
55    println!("\n>> 状態カバレッジテストの実行");
56    let state_results = runner.run_tests(state_tests);
57    print_test_results(&state_results);
58
59    println!("\n>> 遷移カバレッジテストの実行");
60    let transition_results = runner.run_tests(transition_tests);
61    print_test_results(&transition_results);
62
63    // モデル検査
64    println!("\n=== モデル検査 ===");
65    let mut checker = ModelChecker::new(&machine);
66
67    // 到達可能性プロパティ
68    let reachability = Property {
69        name: "赤信号に到達可能か".to_string(),
70        property_type: PropertyType::Reachability,
71        target_states: vec!["red".to_string()],
72        description: Some("赤信号状態に到達できることを確認".to_string()),
73    };
74
75    let result = checker.verify_property(&reachability);
76    println!("\n>> プロパティ: {}", reachability.name);
77    println!(
78        "結果: {}",
79        if result.satisfied {
80            "満たされています"
81        } else {
82            "満たされていません"
83        }
84    );
85    if let Some(msg) = result.message {
86        println!("メッセージ: {}", msg);
87    }
88
89    // 安全性プロパティ
90    let safety = Property {
91        name: "存在しない状態に到達しないか".to_string(),
92        property_type: PropertyType::Safety,
93        target_states: vec!["invalid".to_string()],
94        description: Some("存在しない状態に決して到達しないことを確認".to_string()),
95    };
96
97    let result = checker.verify_property(&safety);
98    println!("\n>> プロパティ: {}", safety.name);
99    println!(
100        "結果: {}",
101        if result.satisfied {
102            "満たされています"
103        } else {
104            "満たされていません"
105        }
106    );
107    if let Some(msg) = result.message {
108        println!("メッセージ: {}", msg);
109    }
110
111    // デッドロックの検出
112    println!("\n>> デッドロック検出");
113    let deadlocks = checker.detect_deadlocks();
114    if deadlocks.is_empty() {
115        println!("デッドロック状態はありません");
116    } else {
117        println!("デッドロック状態: {}", deadlocks.join(", "));
118    }
119
120    // 到達不可能な状態の検出
121    println!("\n>> 到達不可能な状態の検出");
122    let unreachable = checker.detect_unreachable_states();
123    if unreachable.is_empty() {
124        println!("到達不可能な状態はありません");
125    } else {
126        println!("到達不可能な状態: {}", unreachable.join(", "));
127    }
128}

Trait Implementations§

Source§

impl<'a> Debug for ModelChecker<'a>

Source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

impl<'a> Freeze for ModelChecker<'a>

§

impl<'a> !RefUnwindSafe for ModelChecker<'a>

§

impl<'a> Send for ModelChecker<'a>

§

impl<'a> Sync for ModelChecker<'a>

§

impl<'a> Unpin for ModelChecker<'a>

§

impl<'a> !UnwindSafe for ModelChecker<'a>

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.