lmntal / slim

slim LMNtal implementation
Other
18 stars 5 forks source link

コネクタと膜とプロセス文脈に関するバグ #321

Closed nikosai closed 7 months ago

nikosai commented 7 months ago
a(H1),a(H2),{b(H1),b(H2)}.

r1@@ {b(L1),b(L2)} :- {L1=L2}.
r2@@ {} :- .

上記プログラムを通常実行(-tオプション)すると、

1: a(L0). a(L1). {b(L0). b(L1). }. @4. 
---->r1
2: a(L0). a(L0). {}. @4. 
---->r2
3: a(L0). a(L0). @4. 
---->
malloc(): unaligned tcache chunk detected
中止 (コアダンプ)

と言われて異常終了する。

nikosai commented 7 months ago

そもそも、意味論に厳格に従った場合期待される動作(-t --show-proxy)は

1: a($out(L0)). a($out(L1)). {b($in(L0)). b($in(L1)). }. @4. 
---->r1
2: a(L0). a(L0). {$in(L0,$in(L1)). }. @4. 
---->delete_redundant_inproxies (= 遷移規則 (R4) に対応するsystem_ruleset)
3: a(L0). a(L0). {}. @4. 
---->r2
4: a(a). @4.

の3ステップであるが、現状ではinプロキシ2つが存在する膜 {$in(L0,$in(L1)). }. に対してルールr2が発火してしまっている。 これは、コンパイラ側で {} :- をコンパイルする際、「膜内にアトムが存在しない」ことを確かめるためにnatoms命令を吐き出しているが(compile/GuardCompiler.java: countAtomsOfMembrane 関数)、このnatoms命令は「プロキシを除く」アトム数をカウントする仕様となっており、プロキシのみが存在する膜を空として処理してしまっている。

これを(意味論に照らして)正しく処理するには、natoms命令の仕様を変更する必要がある。

nikosai commented 7 months ago

関連するかは不明だが、以下のプログラムは通常実行でSEGVするが、非決定実行ではSEGVしない。

a(H1),a(H2),
{b(H1),b(H2)}.

r1@@ {b(L1),b(L2)} :- {L1=L2}.
r2@@ {$p[L1,L2]} :- uniq | {$p[L1,L2]},{$p[L3,L4]},c(L3),c(L4).
nikosai commented 7 months ago

see also #235

nikosai commented 7 months ago

一時対応策を #331 で実装したが、根本的解決ではないので本Issueは継続検討。