--ltl に --use-Ncore をつけた場合の出力が正しくない

[miuele]

--use-Ncoreをつけない場合はCounterExamplePathsが、--use-Ncoreをつけた場合はNo Accepting Cycle existsと表示されます。

model.lmn

a.
a :- b.
b :- a.

model.nc

never { /* []<>a_exists */
T0_init:
        if
        :: (a_exists) -> goto accept_S1
        :: (1) -> goto T0_init
        fi;
accept_S1:
        if
        :: (a_exists) -> goto accept_S1
        :: (1) -> goto T0_init
        fi;
}

model.psym

a_exists = a

--use-Ncoreをつけない場合

$ slim --ltl-all --psym model.psym --nc model.nc model.lmn
CounterExamplePaths
  1::T0_init{a. @4. }
* 3::accept_S1{b. @4. }
  1::T0_init{a. @4. }
* 3::accept_S1{b. @4. }

'# of States'(stored)   = 3.
'# of States'(end)      = 0.
'# of States'(invalid)  = 0.

--use-Ncore=1をつけた場合（N≧2についても同様）

$ slim --use-Ncore=1 --ltl-all --psym model.psym --nc model.nc model.lmn
No Accepting Cycle (or Invalid State) exists.
'# of States'(stored)   = 3.
'# of States'(end)      = 0.
'# of States'(invalid)  = 0.

[miuele]

slim 2.3.1（私の環境でコンパイルできた最も古いバージョン） と 2.7.0 で確認しました。

[tmp]$ $LMNTAL_HOME/bin/slim --version
Slim Lmntal IMplementation - version 2.7.0 (44f661e6)
[tmp]$ ./slim/bin/slim --version
Slim Lmntal IMplementation - version 2.3.1 (15cb86fa)
[tmp]$ $LMNTAL_HOME/bin/lmntal --version
LMNtal Compiler 1.70 (2024-04-05)

[tmp]$ $LMNTAL_HOME/bin/slim --ltl-all --psym model.psym --nc model.nc model.lmn
CounterExamplePaths
  1::T0_init{a. @4. }
* 3::accept_S1{b. @4. }
  1::T0_init{a. @4. }
* 3::accept_S1{b. @4. }

'# of States'(stored)   = 3.
'# of States'(end)      = 0.
'# of States'(invalid)  = 0.
[tmp]$ $LMNTAL_HOME/bin/slim --use-Ncore=1 --ltl-all --psym model.psym --nc model.nc model.lmn
No Accepting Cycle (or Invalid State) exists.
'# of States'(stored)   = 3.
'# of States'(end)      = 0.
'# of States'(invalid)  = 0.

[tmp]$ ./slim/bin/slim --ltl-all --psym model.psym --nc model.nc model.lmn
CounterExamplePaths
  1::T0_init{a. @4. }
* 3::accept_S1{b. @4. }
  1::T0_init{a. @4. }
* 3::accept_S1{b. @4. }

'# of States'(stored)   = 3.
'# of States'(end)      = 0.
'# of States'(invalid)  = 0.
[tmp]$ ./slim/bin/slim --use-Ncore=1 --ltl-all --psym model.psym --nc model.nc model.lmn
No Accepting Cycle (or Invalid State) exists.
'# of States'(stored)   = 3.
'# of States'(end)      = 0.
'# of States'(invalid)  = 0.

[nikosai]

これはむしろコンパイラの問題であるように見えます。

以下のコミット前後で再現するか否かが変わるようですが、このコミット自体は別に悪いことをしている雰囲気はなく……。
lmntal/lmntal-compiler@df9e16b