GCC:重複定義(Multiple Definition)を許可するオプションを関数単体試験に利用する
このブログでは、現在「GCC:関数重複定義(Multiple Definition)を-z muldefsで許可する - プログラミングなどなど」が見られている回数が圧倒的に多く、全体の約半分を締めています。個人的には使用することが無かったため、なぜ、こんなに見られるのだろうかと気になっていました。そんな中、関数単体試験の際に役立つケースがあったので紹介したいと思います。(やっていることは前の記事と違いはありません。)
以下のような状況を想定しています。
targetModule.cに含まれるtargetFunc関数に大規模な修正を入れることになりました。その際に、同一モジュール内に含まれる長く、複雑な関数longFuncの呼び出しが追加されました。targetFuncの関数単体試験を実施したいのですが、longFuncが同一モジュールに含まれており、邪魔になっています。しかし、別モジュールへの分離も事情により行うことができません。
どの様に役立ったかというと、関数単体試験向けのlongFuncを別モジュールに用意し、リンク時に-z muldefsを使用することで、既存のlongFuncが動作しないようにしました。
targetModule.h
#ifndef TARTGET_MOD #define TARTGET_MOD int longFunc(int x); int targetFunc(int x); #endif
targetModule.c
#include <stdio.h> #include "targetModule.h" /* 長く複雑な関数 */ int longFunc(int x) { printf("長く、複雑な関数!\n"); return x; } /* 修正しテスト対象となる関数 */ int targetFunc(int x) { /* 修正色々 */ /* 同一モジュール内の長く、複雑な関数の呼び出し。*/ int ret = longFunc(10); /* 修正色々 */ return ret + 10; }
test.c
#include <stdio.h> #include "targetModule.h" int main(void) { int ret = targetFunc(5); printf("結果 : %d\n", ret); return 0; }
実行(通常)
$ gcc -Wall targetModule.c test.c $ ./a.out 長く、複雑な関数! 結果 : 20
関数単体試験用のモジュール(test.cに含める方法もあり)
#include <stdio.h> int longFunc(int x) { printf("単体試験用の関数!!\n"); return x; }
実行(スタブ版)
リンク順序には注意します。stub.cに定義した単体試験用のlongFuncが有効になるようにtargetModule.cより前に指定しています。
$ gcc -Wall -z muldefs stub.c targetModule.c test.c $ ./a.out 単体試験用の関数!! 結果 : 10
これまでは、デバッガなどを使って行っていた試験が自動化できました。
Haskell:whereとletを使った関数定義のスタイルについて(Stateモナド手前のfmap)
7/22から7/25と4連休だったのと、SPINからちょっと離れたいとの思いから、HaskellのFunctorからMonadの流れを勉強してみようと思い本(プログラミングHaskell 第2版)を読んでいました。読み進める中でStateモナドを定義する前のFunctorのfmap実装がぱっと理解できずに別の書籍(関数プログラミング入門 ―Haskellで学ぶ原理と技法―)にあたったのですが、こういう風に書かれていたら、個人的にはわかりやすかったかもな。と思う部分がありましたので、載せたいと思います。まぁ、慣れれば、どちらでも良いのでしょうが。
共通部分
newtype St a = MkSt (State -> (a, State)) type State = Int app :: St a -> State -> (a, State) app (MkSt stf) s = stf s
例1 : 「プログラミング Haskell 第2版」風
instance Functor St where -- fmap :: (a -> b) -> St a -> St b fmap f sta = MkSt (\s -> let (x, s') = app sta s in (f x, s'))
letを使って上から下に読める感じは好きなのですが、\s -> ... の部分が慣れないせいか、すっと頭に入りませんでした。
例2 : 「関数プログラミング入門 -Haskellで学ぶ原理と技法-」風
本の中では、StのFunctorインスタンスの定義はなく、Monadの定義のみが出てきていますが、この本の記述スタイルならこうなるだろという風で書いています。
instance Functor St where -- fmap :: (a -> b) -> St a -> St b fmap f sta = MkSt g where g s = (f x, s') where (x, s') = app sta s
例1と少し変わって、MkSt g と g s = ... でsを引数にとる関数を定義し返している部分は、わかりやすい感じで好きなのですが、
... = (f x, s')
where (x, s') = app staの部分は下の定義を確認して上に戻らなければならないので、部分でちょっと好きになれませんでした。
例3 : 混ぜた感じ
個人的には、例1,2を混ぜた感じの以下の様な記述だと、すっと入りそうな気がしました。
instance Functor St where -- fmap :: (a -> b) -> St a -> St b fmap f sta = MkSt g where g s = let (x, s') = app sta s in (f x, s')
SPIN:Never Claimと通常プロセスの動作の違いに気をつけよう
SPINでは検証式の記述に時相論理という論理が使えるのですが、よく理解できなかったので簡単なものから理解していこうと考えました。しかし、単純と思いきやハマった例を紹介します。ハマった部分を確認しようとしましたが、結果としては現状、手詰まりとなりました。
モデル(never.pml)
以下のようなモデルと検証式があるとします。
bool i = false; active proctype A() { i = true; } ltl { i == false }
検証の実行
上記のLTLの検証結果を予想してみて下さい。
$ spin -run never.pml
(Spin Version 6.5.0 -- 17 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 20 byte, depth reached 0, errors: 0
1 states, stored
0 states, matched
1 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype A
never.pml:6, state 2, "-end-"
(1 of 2 states)
unreached in claim ltl_0
_spin_nvr.tmp:8, state 8, "-end-"
(1 of 8 states)
pan: elapsed time 0 seconds私はエラーが検出されると想定しました。しかし、エラー無しとなりました。
記述したLTLのPromelaコードの確認
以下のコマンドを実行し、記述したLTLからどの様なNever ClaimがPromeralコードとして生成されたかを確認してみます。
$ spin -a never.pml
ltl ltl_0: (i==0)
$ cat -n _spin_nvr.tmp
1 never ltl_0 { /* !((i==0)) */
2 accept_init:
3 T0_init:
4 do
5 :: atomic { (! (((i==0)))) -> assert(!(! (((i==0))))) }
6 od;
7 accept_all:
8 skip
9 }現状の私の理解は次のとおりです。
- 5行目の!(((i==0)))はプロセスAのi = trueが実行されるまでは、成立しないので、do文で実行可能な処理がなくブロックされる。
- プロセスAのi = trueが実行されると、Never Claimの!(((i==0)))が成立し、assertが実行されエラーが検出される。
しかし、エラーは検出されませんでした。
LTLのPromelaコードから通常プロセスを作る
現状、私は通常プロセスとNever Claimの違いについて、Never Claimは検証対象のプロセスの1ステップ毎にNever Claimの検証を行う。と理解しています。
そこで、得られたPromelaコードを通常プロセスとして実装した場合、検証漏れはあるかもしれませんが、今回のケースでは網羅的な検証でエラーが無いことになっているので、通常プロセスにしても0件になるのではないかと予想し試すことにしました。
追記したコード
ltlの部分を以下のコードに置き換えます。
active proctype B() { /* !((i==0)) */ accept_init: T0_init: do :: atomic { (! (((i==0)))) -> assert(!(! (((i==0))))) } od; accept_all: skip }
検証の実行
$ spin -run never.pml
pan:1: assertion violated !( !((i==0))) (at depth 1)
pan: wrote never.pml.trail
(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
acceptance cycles + (fairness disabled)
invalid end states +
State-vector 20 byte, depth reached 1, errors: 1
2 states, stored
0 states, matched
2 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
pan: elapsed time 0 secondsなんと、エラーを検出しました。今のPromelaコードの理解としてはこちらの方がしっくりくるのですが、Never Claimの動作理解としては、ここでお手上げとなりました。
状態テーブルに違があるかを確認
他に差異があるかを確認できないかと考えて状態表(-dオプション)を比べて見ましたが、同じでした。
Never Claim
$ ./pan -d
proctype A
state 1 -(tr 5)-> state 2 [id 0 tp 2] [----G] never.pml:5 => i = 1
state 2 -(tr 6)-> state 0 [id 1 tp 3500] [--e-L] never.pml:6 => -end-
claim ltl_0
state 4 -(tr 3)-> state 4 [id 2 tp 2] [-a--G] never.pml:4 => (!((i==0)))
Transition Type: A=atomic; D=d_step; L=local; G=global
Source-State Labels: p=progress; e=end; a=accept;
Note: statement merging was used. Only the first
stmnt executed in each merge sequence is shown
(use spin -a -o3 to disable statement merging)
pan: elapsed time 1.72e+07 seconds
pan: rate 0 states/second
通常プロセス
$ ./pan -d
proctype A
state 1 -(tr 5)-> state 2 [id 0 tp 2] [----G] never.pml:5 => i = 1
state 2 -(tr 6)-> state 0 [id 1 tp 3500] [--e-L] never.pml:6 => -end-
proctype B
state 4 -(tr 3)-> state 4 [id 2 tp 2] [-a--G] never.pml:12 => (!((i==0)))
Transition Type: A=atomic; D=d_step; L=local; G=global
Source-State Labels: p=progress; e=end; a=accept;
Note: statement merging was used. Only the first
stmnt executed in each merge sequence is shown
(use spin -a -o3 to disable statement merging)
pan: elapsed time 1.72e+07 seconds
pan: rate 0 states/second
結果(手詰まり)
自分は手詰まりとなりました。前回の記事(SPIN:LTLの記述によっては意図した検査にならない? - プログラミングなどなど)のようにデバッグしてみると、Never Claimの遷移処理が走っていますが、どこにも遷移せずにすぐに検証が終了していました。感覚としては、検証時の最初のステップでNever Claimがどこにも移動できないような記述がある時に問題となるケースがありそうです。自分のLTLの記述が悪い感じもありますが。
SPIN:LTLの記述によっては意図した検査にならない?
前回モデル(SPIN:モデル(安全性(排他)と応答性) - プログラミングなどなど)でLTLで検証式を記述する際に実は、トライ&エラーを行っていました。その際、記述したLTLで想定していた検査が行われていないようなケースがありました。
そもそも、記述したLTLが誤っているかもしれないので、慣れている人やよく理解している人には無縁かもしれませんが、私は最初気がつかなかったので、メモとして残したいと思います。
モデル(model.pml)(前回と同じもの)
/* OPE-SV間のメッセージ定義 */ mtype = { START_SND_SRV, /* 第2サービス開始 */ STOP_SND_SRV /* 第2サービス停止 */ } /* SVとの通信用チャネル */ chan svCh = [2] of { mtype } /* 運用者による操作を受付てSVに操作に対応するメッセージを送信するプロセス */ active proctype OPE() { bool sndSrvOrd = false; /* 運用者による第2サービス開始操作 */ atomic { sndSrvOrd = true; svCh ! START_SND_SRV; } /* 時間経過などもろもろ */ /* 運用者による第2サービス停止操作 */ atomic { sndSrvOrd = false; svCh ! STOP_SND_SRV; } } /* 実際のサービスを制御するサーバプロセス */ active proctype SV() { /* デフォルトでは第1サービスが有効になっているものとする。*/ /* 運用者から第2サービスの開始操作が行われた場合に、 第2サービスを開始する。*/ /* 第1サービスと第2サービスは排他関係になっており、両者が共に有効になってはならない。*/ bool isFstSrvOn = true; bool isSndSrvOn = false; mtype event; do :: svCh ? event -> if :: atomic { event == START_SND_SRV -> isFstSrvOn = false; isSndSrvOn = true; } :: atomic { event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false; } fi od }
前回の検証式
前回は、運用者からの第2サービスの開始にともなって第2サービスが有効になること。また、停止に伴って第2サービスが停止することを、応答性として以下の様に記述しました。
応答性(第2サービス開始)
/* 運用者による第2サービスの開始操作が行われたら、第2サービスが有効になる。*/ ltl liveSndStart { [](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) }
応答性2(第2サービス停止)
/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になる。*/ ltl liveSndStop { [](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) }
検証式(誤り?)
上記の形になる試行錯誤の前は以下の様に記述していました。
注目して頂きたいのは前提条件(OPE:sndSrvOrd == true, OPE:sndSrvOrd == false)の部分となります。
例1
/* 運用者による第2サービスの開始操作が行われたら、第2サービスが有効になる。*/ ltl liveSndStart2 { OPE:sndSrvOrd == true -> <>[](SV:isSndSrvOn == true) } ltl nliveSndStart2 { !(OPE:sndSrvOrd == true -> <>[](SV:isSndSrvOn == true)) }
例2
/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になる。*/ ltl liveSndStop2 { OPE:sndSrvOrd == false -> <>[](SV:isFstSrvOn == true) } ltl nliveSndStop2 { !(OPE:sndSrvOrd == false -> <>[](SV:isFstSrvOn == true)) }
検証の実行
例1
例１の検証を実行してみると、確かにエラーが0件であることは想定どおりなのですが、「1 states, stored」となっていたり、「unreached」に実行を想定している行が出力されていたりと怪しい感じが出ています。
$ spin -run -ltl liveSndStart2 model.pml
pan: ltl formula liveSndStart2
(Spin Version 6.5.0 -- 17 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (liveSndStart2)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 52 byte, depth reached 0, errors: 0
1 states, stored
0 states, matched
1 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.261 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype OPE
model.pml:16, state 2, "svCh!START_SND_SRV"
model.pml:21, state 5, "svCh!STOP_SND_SRV"
model.pml:21, state 6, "sndSrvOrd = 0"
model.pml:22, state 7, "-end-"
(4 of 7 states)
unreached in proctype SV
model.pml:37, state 3, "isFstSrvOn = 0"
model.pml:37, state 4, "isSndSrvOn = 1"
model.pml:38, state 7, "isFstSrvOn = 1"
model.pml:38, state 8, "isSndSrvOn = 0"
model.pml:37, state 10, "((event==START_SND_SRV))"
model.pml:37, state 10, "((event==STOP_SND_SRV))"
model.pml:41, state 15, "-end-"
(6 of 15 states)
unreached in claim liveSndStart2
_spin_nvr.tmp:101, state 10, "(1)"
_spin_nvr.tmp:105, state 17, "(!((SV.isSndSrvOn==1)))"
_spin_nvr.tmp:105, state 17, "(1)"
_spin_nvr.tmp:108, state 20, "-end-"
(3 of 20 states)
pan: elapsed time 0 seconds
例2
因みに例2を実行した場合は、ちゃんと探索してくれていそうな感じがあります。
$ spin -run -ltl liveSndStop2 model.pml
pan: ltl formula liveSndStop2
(Spin Version 6.5.0 -- 17 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (liveSndStop2)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 52 byte, depth reached 20, errors: 0
12 states, stored (17 visited)
9 states, matched
26 transitions (= visited+matched)
20 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.001 equivalent memory usage for states (stored*(State-vector + overhead))
0.261 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype OPE
(0 of 7 states)
unreached in proctype SV
model.pml:41, state 15, "-end-"
(1 of 15 states)
unreached in claim liveSndStop2
_spin_nvr.tmp:143, state 20, "-end-"
(1 of 20 states)
pan: elapsed time 0 seconds
デバッグ
例1で探索が行われていないのかを部分を見たいと考えデバッグしてみることにしました。検証器のコンパイルまでに行った手順は以下となります。
検証器コードの整形とデバッグオプション付きでのコンパイル
$ spin -a model.pml ltl safe: [] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1)))) : ltl nliveSndStart3: ! ([] (<> ((! ((OPE:sndSrvOrd==1))) || (<> ([] ((SV:isSndSrvOn==1))))))) the model contains 13 never claims: nliveSndStart3, liveSndStart3, nliveSndStop2, liveSndStop2, nliveSndStart2, liveSndStart2, nliveSndStop, liveSndStop, nliveSndStart, liveSndStart, notStop, nsafe, safe only one claim is used in a verification run choose which one with ./pan -a -N name (defaults to -N safe) or use e.g.: spin -search -ltl safe model.pml $ gcc -E -C -P -DNOREDUCE pan.c > ppan.c $ indent ppan.c -o pppan.c $ gcc -g3 -O0 pppan.c
GDBによるデバッグ
do_transit関数にブレークポイントを設定しステップ実行していくと、確かにすぐに検証を完了したルートに入っていそうでした。
$ gdb --args ./a.out -a -N liveSndStart2
(gdb) break do_transit
Breakpoint 1 at 0x6d09: file pppan.c, line 9653.
(gdb) r
Starting program: /home/makoto/blog/ltlNG/a.out -a -N liveSndStart2
pan: ltl formula liveSndStart2
Breakpoint 1, do_transit (t=0x19010, II=32767) at pppan.c:9653
9653 {
(gdb) backtrace
#0 do_transit (t=0x19010, II=32767) at pppan.c:9653
#1 0x0000555555561645 in new_state () at pppan.c:11685
#2 0x000055555555acf2 in do_the_search () at pppan.c:9648
#3 0x00005555555587e0 in run () at pppan.c:8945
#4 0x000055555556485d in main (argc=1, argv=0x7fffffffdd80) at pppan.c:13316上記設定後に処理を再開させてステップ実行させていくと、他状態への遷移がなく、すぐにrun関数から戻り、結果の出力処理へと進みました。
SPIN:モデル(安全性(排他)と応答性)
LTLに少し慣れた気がしたので、簡単なモデルを記述し練習してみることにしました。
モデルとしては、サーバでは標準で第1サービスが有効になっているが、運用者から第2サービスの開始操作があった場合に、サービスを切り替えるというものです。サービスは排他関係になっており、第1と第2サービスがともに有効になってはならないものとしています。検査の範囲としては、運用者が第2サービスを開始操作を行い、その後、停止操作を行うという流れを考えています。
モデル(model.pml)
/* OPE-SV間のメッセージ定義 */ mtype = { START_SND_SRV, /* 第2サービス開始 */ STOP_SND_SRV /* 第2サービス停止 */ } /* SVとの通信用チャネル */ chan svCh = [2] of { mtype } /* 運用者による操作を受付てSVに操作に対応するメッセージを送信するプロセス */ active proctype OPE() { bool sndSrvOrd = false; /* 運用者による第2サービス開始操作 */ atomic { sndSrvOrd = true; svCh ! START_SND_SRV; } /* 時間経過などもろもろ */ /* 運用者による第2サービス停止操作 */ atomic { sndSrvOrd = false; svCh ! STOP_SND_SRV; } } /* 実際のサービスを制御するサーバプロセス */ active proctype SV() { /* デフォルトでは第1サービスが有効になっているものとする。*/ /* 運用者から第2サービスの開始操作が行われた場合に、 第2サービスを開始する。*/ /* 第1サービスと第2サービスは排他関係になっており、両者が共に有効になってはならない。*/ bool isFstSrvOn = true; bool isSndSrvOn = false; mtype event; do :: svCh ? event -> if :: atomic { event == START_SND_SRV -> isFstSrvOn = false; isSndSrvOn = true; } :: atomic { event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false; } fi od }
検証式の追加
先頭にnが付いているものは、動作確認用にエラーを出力させるために用意しました。
安全性
/* 第1サービスと第2サービスが共に有効で無い状態が、常に成り立つ。*/ ltl safe { []!(SV:isFstSrvOn == true && SV:isSndSrvOn == true) } ltl nsafe { ![]!(SV:isFstSrvOn == true && SV:isSndSrvOn == true) } /* 第1サービスと第2サービスが共に無効な状態は、常に成立しない。*/ /* -> どちらかのサービスは有効である。*/ ltl notStop { []!(SV:isFstSrvOn == false && SV:isSndSrvOn == false) }
応答性(第2サービス開始)
/* 運用者による第2サービスの開始操作が行われたら、第1サービスが無効になり、第2サービスが有効になる。*/ ltl liveSndStart { [](OPE:sndSrvOrd == true -> <>(SV:isFstSrvOn == false && SV:isSndSrvOn == true)) } ltl nliveSndStart { ) }
応答性2(第2サービス停止)
/* 運用者による第2サービスの停止操作が行われたら、第1サービスが有効になり、第2サービスが無効になる。*/ ltl liveSndStop { [](OPE:sndSrvOrd == false -> <>(SV:isFstSrvOn == true && SV:isSndSrvOn == false)) } ltl nliveSndStop { ) }
試し
試しにSVがSTOP_SND_SRVイベントの処理を行う部分のatomicを取り除き以下の様にしてみます。
// :: atomic { event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false; } :: event == STOP_SND_SRV -> isFstSrvOn = true; isSndSrvOn = false;
すると、安全性の検査でisFstSrvOnとisSndSrvOnの両方がtrueになるケースがエラーとして検出されます。
検出例
$ spin -t -p -l model.pml
pan: ltl formula safe
pan:1: assertion violated !( !( !(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1))))) (at depth 19)
pan: wrote model.pml.trail
(Spin Version 6.5.0 -- 17 July 2019)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim + (safe)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 44 byte, depth reached 19, errors: 1
8 states, stored
0 states, matched
8 transitions (= stored+matched)
5 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.001 equivalent memory usage for states (stored*(State-vector + overhead))
0.278 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
pan: elapsed time 0 seconds$ spin -t -p -l model.pml ltl safe: [] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1)))) ltl nsafe: ! ([] (! (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==1))))) ltl notStop: [] (! (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==0)))) ltl liveSndStart: [] ((! ((OPE:sndSrvOrd==1))) || (<> (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==1))))) ltl nliveSndStart: ! ([] ((! ((OPE:sndSrvOrd==1))) || (<> (((SV:isFstSrvOn==0)) && ((SV:isSndSrvOn==1)))))) ltl liveSndStop: [] ((! ((OPE:sndSrvOrd==0))) || (<> (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==0))))) ltl nliveSndStop: ! ([] ((! ((OPE:sndSrvOrd==0))) || (<> (((SV:isFstSrvOn==1)) && ((SV:isSndSrvOn==0)))))) starting claim 2 Never claim moves to line 4 [(1)] 2: proc 0 (OPE:1) model.pml:16 (state 1) [sndSrvOrd = 1] OPE(0):sndSrvOrd = 1 3: proc 0 (OPE:1) model.pml:16 (state 2) [svCh!START_SND_SRV] 5: proc 1 (SV:1) model.pml:35 (state 1) [svCh?event] SV(1):event = START_SND_SRV 7: proc 1 (SV:1) model.pml:37 (state 2) [((event==START_SND_SRV))] 8: proc 1 (SV:1) model.pml:37 (state 3) [isFstSrvOn = 0] SV(1):isFstSrvOn = 0 9: proc 1 (SV:1) model.pml:37 (state 4) [isSndSrvOn = 1] SV(1):isSndSrvOn = 1 11: proc 0 (OPE:1) model.pml:21 (state 4) [sndSrvOrd = 0] OPE(0):sndSrvOrd = 0 12: proc 0 (OPE:1) model.pml:21 (state 5) [svCh!STOP_SND_SRV] 14: proc 1 (SV:1) model.pml:35 (state 1) [svCh?event] SV(1):event = STOP_SND_SRV 16: proc 1 (SV:1) model.pml:39 (state 6) [((event==STOP_SND_SRV))] 18: proc 1 (SV:1) model.pml:39 (state 7) [isFstSrvOn = 1] SV(1):isFstSrvOn = 1 Never claim moves to line 3 [(!(!(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1)))))] spin: _spin_nvr.tmp:3, Error: assertion violated spin: text of failed assertion: assert(!(!(!(((SV.isFstSrvOn==1)&&(SV.isSndSrvOn==1)))))) spin: trail ends after 20 steps #processes: 2 queue 1 (svCh): 20: proc 1 (SV:1) model.pml:39 (state 8) SV(1):event = STOP_SND_SRV SV(1):isSndSrvOn = 1 SV(1):isFstSrvOn = 1 20: proc 0 (OPE:1) model.pml:22 (state 7) <valid end state> OPE(0):sndSrvOrd = 0 20: proc - (safe:1) _spin_nvr.tmp:2 (state 6) 2 processes created
SPIN:2プロセスからのメッセージ受信順序確認
前回(SPIN:LTLを使った2プロセスの実行順序確認 - プログラミングなどなど)の内容と似ていますが、今度は2つのプロセスA,BがプロセスCにメッセージ送信する例を考えてみました。前回の内容とほぼ同じなので、同じオプションで結果が得られると考えていましたが、Bが先に送信するケースだけが検出されトライ&エラーを繰り返すこととなりました。
結果として、最適化オプションの無効化-o1または-o2を行うことで欲しいケースを得ることができました。(結果以上のことは理解していません。)
モデル
$ cat -n 2msg.pml
1 mtype = { msgA, msgB }
2
3 chan ch = [2] of { mtype }
4
5 bool isRcvA = false;
6 bool isRcvB = false;
7
8 active proctype A()
9 {
10 ch ! msgA
11 }
12
13 active proctype B()
14 {
15 ch ! msgB
16 }
17
18 active proctype C()
19 {
20 mtype msg;
21 do
22 :: ch ? msg ->
23 if
24 :: msg == msgA -> isRcvA = true;
25 :: msg == msgB -> isRcvB = true;
26 fi
27 od
28 }プロセスAとBが、プロセスCに向けてメッセージを送信するモデルです。実行の制約は無いので、22行目:プロセスCのch ? msg では、msgAを先に受信する場合とmsgBを先に受信する場合があるはずです。
ランダムシミュレーション
ランダムシミュレーションを何度か行ってみると、確かに上記の2ケースが結果として出てきます。
msgAを先に受信するケース
$ spin -r 2msg.pml
3: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch)
8: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch)
timeout
#processes: 3
queue 1 (ch):
isRcvA = 1
isRcvB = 1
12: proc 2 (C:1) 2msg.pml:21 (state 8)
12: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state>
12: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state>
3 processes created
msgBを先に受信するケース
$ spin -r 2msg.pml
3: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch)
8: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch)
timeout
#processes: 3
queue 1 (ch):
isRcvA = 1
isRcvB = 1
12: proc 2 (C:1) 2msg.pml:21 (state 8)
12: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state>
12: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state>
3 processes created
LTLでの確認
確認したい性質としては先の例と同じなので同様の式を追加して検証してみます。
検証式
以下の検証式をモデルに追加します。
検証したい性質
ltl a01 { <>[](isRcvA == true && isRcvB == true) }
検証したい性質の否定
ltl c01 { !<>[](isRcvA == true && isRcvB == true) }
実行
検証したい性質の確認
$ spin -run -ltl a01 2msg.pml
pan: ltl formula a01
(Spin Version 6.5.0 -- 17 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (a01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 44 byte, depth reached 17, errors: 0
43 states, stored (83 visited)
83 states, matched
166 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.003 equivalent memory usage for states (stored*(State-vector + overhead))
0.289 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype A
(0 of 2 states)
unreached in proctype B
(0 of 2 states)
unreached in proctype C
2msg.pml:28, state 11, "-end-"
(1 of 11 states)
unreached in claim a01
_spin_nvr.tmp:10, state 13, "-end-"
(1 of 13 states)
unreached in claim c02
_spin_nvr.tmp:19, state 10, "(((isRcvA==1)&&(isRcvB==1)))"
_spin_nvr.tmp:21, state 13, "-end-"
(2 of 13 states)
pan: elapsed time 0 seconds
検証したい性質がどのように成り立ったかの確認
$ spin -run -ltl c01 -c0 -e 2msg.pml
pan: ltl formula c01
pan:1: acceptance cycle (at depth 18)
pan: wrote 2msg.pml1.trail
pan: wrote 2msg.pml2.trail
(Spin Version 6.5.0 -- 17 July 2019)
+ Partial Order Reduction
Full statespace search for:
never claim + (c01)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 44 byte, depth reached 18, errors: 2
23 states, stored (24 visited)
8 states, matched
32 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.002 equivalent memory usage for states (stored*(State-vector + overhead))
0.289 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype A
(0 of 2 states)
unreached in proctype B
(0 of 2 states)
unreached in proctype C
2msg.pml:28, state 11, "-end-"
(1 of 11 states)
unreached in claim c01
_spin_nvr.tmp:21, state 13, "-end-"
(1 of 13 states)
pan: elapsed time 0 seconds
エラートレイルの確認
エラートレイルを確認すると検出された2件ともmsgBを先に受信したケースとなっています。
1件目
$ spin -t1 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10)
2件目
$ spin -t2 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
トライ&エラー
検証式はあっているだろうとの考えから、今回はオプションが関係していないかと思い--helpオプションで出力される内容から該当しそうなものを試していきました。
試した結果、詳しい理由はわかりませんが以下のオプションを使用することで、msgAから受信するケースとmsgBから受信するケースの両方を検出させることができました。
オプション -o1 turn off dataflow-optimizations in verifier
$ spin -o1 -run -ltl c01 -c0 -e 2msg.pml
:
State-vector 44 byte, depth reached 18, errors: 4
25 states, stored (27 visited)
10 states, matched
37 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
msgBから受信するケース
$ spin -t1 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
msgBから受信するケース
$ spin -t3 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
オプション -o2 don't hide write-only variables in verifier
$ spin -o2 -run -ltl c01 -c0 -e 2msg.pml
:
State-vector 44 byte, depth reached 18, errors: 4
25 states, stored (27 visited)
10 states, matched
37 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
msgBから受信するケース
$ spin -t1 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
msbAから受信するケース
$ spin -t3 -r 2msg.pml ltl a01: <> ([] (((isRcvA==1)) && ((isRcvB==1)))) ltl c01: ! (<> ([] (((isRcvA==1)) && ((isRcvB==1))))) starting claim 4 Never claim moves to line 15 [(1)] 4: proc 2 (C:1) 2msg.pml:22 Recv msgA <- queue 1 (ch) 12: proc 2 (C:1) 2msg.pml:22 Recv msgB <- queue 1 (ch) Never claim moves to line 14 [(((isRcvA==1)&&(isRcvB==1)))] Never claim moves to line 19 [(((isRcvA==1)&&(isRcvB==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 19 steps #processes: 3 queue 1 (ch): isRcvA = 1 isRcvB = 1 19: proc 2 (C:1) 2msg.pml:21 (state 8) 19: proc 1 (B:1) 2msg.pml:16 (state 2) <valid end state> 19: proc 0 (A:1) 2msg.pml:11 (state 2) <valid end state> 19: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 3 processes created
SPIN:LTLを使った2プロセスの実行順序確認
SPINでは記述したモデルについてLTLで記述した性質の検証を行うことで反例がないかどうかをチェックしてくれます。私はまだ理解が浅いのでLTLで記述した検証が意図したものになっているかどうかについて自信がありません。そこで、記述した検証が、意図した検証になっていそうだということを確かめたいと思いました。
結論としては解をつかめていないのですが、大丈夫そうだと思える部分まで行くことができましたので、行った手順とメモを残します。
モデルとしては、2つのプロセスがそれぞれが管理する変数を更新するパターンが2通りあるということを検出したいと思います。
モデル
$ cat -n 2pro.pml
1 bool isAProced = false;
2 bool isBProced = false;
3
4 active proctype A()
5 {
6 isAProced = true;
7 }
8
9 active proctype B()
10 {
11 isBProced = true;
12 }
プロセスAとBがあり、並列に動作するモデルです。実行の制約は無いので、6行目:プロセスAのisAProced = trueが先に実行される場合と11行目:プロセスBのisBProced = trueが先に実行される場合があるはずです。
ランダムシミュレーション
ランダムシミュレーションを何度か行ってみると、確かに上記の2ケースが結果として出てきます。
プロセスAの処理が先に実行されるケース
$ spin -p 2pro.pml 0: proc - (:root:) creates proc 0 (A) 0: proc - (:root:) creates proc 1 (B) 1: proc 0 (A:1) 2pro.pml:6 (state 1) [isAProced = 1] 2: proc 1 (B:1) 2pro.pml:11 (state 1) [isBProced = 1] 2: proc 1 (B:1) terminates 2: proc 0 (A:1) terminates 2 processes created
プロセスBの処理が先に実行されるケース
$ spin -p 2pro.pml 0: proc - (:root:) creates proc 0 (A) 0: proc - (:root:) creates proc 1 (B) 1: proc 1 (B:1) 2pro.pml:11 (state 1) [isBProced = 1] 1: proc 1 (B:1) terminates 2: proc 0 (A:1) 2pro.pml:6 (state 1) [isAProced = 1] 2: proc 0 (A:1) terminates 2 processes created
LTLでの確認
上記のモデルではプロセスA,Bのどちらが先に実行されても最終的にisAProced == true && isBProced == trueが成立します。成立する性質の否定を使って、プロセスAから実行される場合とプロセスBから実行される場合を検出させたいと思います。
検証式
以下の検証式をモデルに追加します。
検証したい性質
ltl a01 { <>[](isAProced == true && isBProced == true) }
検証したい性質の否定
ltl c01 { !<>[](isAProced == true && isBProced == true) }
実行
検証したい性質の確認
$ spin -run -ltl a01 2pro.pml pan: ltl formula a01 (Spin Version 6.5.0 -- 17 July 2019) + Partial Order Reduction Full statespace search for: never claim + (a01) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 28 byte, depth reached 9, errors: 0 12 states, stored (21 visited) 13 states, matched 34 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.001 equivalent memory usage for states (stored*(State-vector + overhead)) 0.290 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 128.730 total actual memory usage unreached in proctype A (0 of 2 states) unreached in proctype B (0 of 2 states) unreached in claim a01 _spin_nvr.tmp:10, state 13, "-end-" (1 of 13 states) unreached in claim c01 _spin_nvr.tmp:19, state 10, "(((isAProced==1)&&(isBProced==1)))" _spin_nvr.tmp:21, state 13, "-end-" (2 of 13 states) pan: elapsed time 0 seconds
検証したい性質がどのように成り立ったかの確認
実行してみるとエラーが3件検出されます。私の理想としては、2件の検出なのですがどの様な式にすればよいのかわかりませんでした。
$ spin -run -ltl c01 -c0 -e 2pro.pml pan: ltl formula c01 pan:1: acceptance cycle (at depth 8) pan: wrote 2pro.pml1.trail pan: wrote 2pro.pml2.trail pan: wrote 2pro.pml3.trail (Spin Version 6.5.0 -- 17 July 2019) + Partial Order Reduction Full statespace search for: never claim + (c01) assertion violations + (if within scope of claim) acceptance cycles + (fairness disabled) invalid end states - (disabled by never claim) State-vector 28 byte, depth reached 9, errors: 3 9 states, stored (11 visited) 7 states, matched 18 transitions (= visited+matched) 0 atomic steps hash conflicts: 0 (resolved) Stats on memory usage (in Megabytes): 0.000 equivalent memory usage for states (stored*(State-vector + overhead)) 0.290 actual memory usage for states 128.000 memory used for hash table (-w24) 0.534 memory used for DFS stack (-m10000) 128.730 total actual memory usage unreached in proctype A (0 of 2 states) unreached in proctype B (0 of 2 states) unreached in claim c01 _spin_nvr.tmp:21, state 13, "-end-" (1 of 13 states) pan: elapsed time 0 seconds
エラートレイルの確認
プロセスBの処理が先に実行されるケース
$ spin -t1 -p 2pro.pml ltl a01: <> ([] (((isAProced==1)) && ((isBProced==1)))) ltl c01: ! (<> ([] (((isAProced==1)) && ((isBProced==1))))) starting claim 3 Never claim moves to line 15 [(1)] 2: proc 1 (B:1) 2pro.pml:11 (state 1) [isBProced = 1] 4: proc 1 terminates 6: proc 0 (A:1) 2pro.pml:6 (state 1) [isAProced = 1] Never claim moves to line 14 [(((isAProced==1)&&(isBProced==1)))] 8: proc 0 terminates <<<<<START OF CYCLE>>>>> Never claim moves to line 19 [(((isAProced==1)&&(isBProced==1)))] spin: trail ends after 10 steps #processes: 0 isAProced = 1 isBProced = 1 10: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 2 processes created $ spin -t2 -p 2pro.pml ltl a01: <> ([] (((isAProced==1)) && ((isBProced==1)))) ltl c01: ! (<> ([] (((isAProced==1)) && ((isBProced==1))))) starting claim 3 Never claim moves to line 15 [(1)] 2: proc 1 (B:1) 2pro.pml:11 (state 1) [isBProced = 1] 4: proc 1 terminates 6: proc 0 (A:1) 2pro.pml:6 (state 1) [isAProced = 1] Never claim moves to line 14 [(((isAProced==1)&&(isBProced==1)))] 8: proc 0 terminates Never claim moves to line 19 [(((isAProced==1)&&(isBProced==1)))] <<<<<START OF CYCLE>>>>> spin: trail ends after 10 steps #processes: 0 isAProced = 1 isBProced = 1 10: proc - (c01:1) _spin_nvr.tmp:18 (state 10) 2 processes created
プロセスAの処理が先に実行されるケース
$ spin -t3 -p 2pro.pml
ltl a01: <> ( (((isAProced==1)) && ((isBProced==1))))
ltl c01: ! (<> ( (((isAProced==1)) && ((isBProced==1)))))
starting claim 3
Never claim moves to line 15 [(1)]
2: proc 0 (A:1) 2pro.pml:6 (state 1) [isAProced = 1]
4: proc 1 (B:1) 2pro.pml:11 (state 1) [isBProced = 1]
Never claim moves to line 14 [(((isAProced==1)&&(isBProced==1)))]
6: proc 1 terminates
Never claim moves to line 19 [(((isAProced==1)&&(isBProced==1)))]
8: proc 0 terminates
spin: trail ends after 8 steps
#processes: 0
isAProced = 1
isBProced = 1
8: proc - (c01:1) _spin_nvr.tmp:18 (state 10)
2 processes created
トライ&エラー
上記の結果が得られるまで、あ〜だ。こ〜だ。とトライ&エラーを繰り返しました。今後の役に立ちそうだったので残しておきます。
常に失敗させる
以下の様なLTLを記述して常に失敗させました。結果としては、18のエラーが検出されました。中身を確認すると、確かに欲しい結果が入っていたので、これを元に検証したい性質でエラーが出るように進めました。
/* errors: 18 */
ltl l01 { false }
改良1
ゴールにすこし近づくように以下を記述しました。なぜ、エラー検出数が異なるのかは、まだ理解できていません。
/* errors: 6 */ ltl l02 { !<>(isAProced == true) } /* errors: 7 */ ltl l03 { !<>(isBProced == true) }
改良2
さらにゴールに近づけました。
これに[]を追加したものが最初に紹介した検証式となります。
/* errors: 5 */ ltl l04 { !<>(isAProced == true && isBProced == true) }
