メタインタプリタの状態数バグ

developでメタインタプリタの状態空間構築を行った時に状態数がslimと異なる

メタインタプリタ


:-  uniq |
ret = run({
    ':-'({p_thinking(!Lx0, !Rx0), fork_free(!Lx1, !Rx0)}, {}, {p_one_fork(!Lx0, !Rx1), fork_used(!Lx1, !Rx1)}),
    ':-'({p_one_fork(!Lxx0, !Rxx0), fork_used(!Lxx1, !Rxx0), fork_free(!Lxx0, !Rxx1)}, {}, {p_eating(!Lxx2, !Rxx2), fork_used(!Lxx1, !Rxx2), fork_used(!Lxx2, !Rxx1)}),
    ':-'({p_eating(!Lxxx0, !Rxxx0), fork_used(!Lxxx0, !Rxxx1), fork_used(!Lxxx1, !Rxxx0)}, {}, {p_thinking(!Lxxx2, !Rxxx2), fork_free(!Lxxx2, !Rxxx1), fork_free(!Lxxx1, !Rxxx2)})
          },
      {
p_thinking(L0, R0), fork_free(L0, R1).
p_thinking(L1, R1), fork_free(L1, R2).
p_thinking(L2, R2), fork_free(L2, R0).
      }).

set.use. state_space.use. n(0), t(0). run@@Ret = run(Rs, {$ini[]}), n($n) :- $nn = $n+1 | Ret = exp0(Rs, s(ID, {$ini[]}), state_space.state_map_find(state_space.state_map_init, {$ini[]}, ID), set.init, set.init), n($nn).

exp0@@Ret = exp0(Rs, S0, Map, Ss, Ts), S0=s($id, {$ini[]}) :- int($id) | Ret = exp(Rs, [s($id, {$ini[]})], Map, set.insert(Ss, $id), Ts), ini($id).

exp@@Ret = exp(Rs, S0, Map, Ss, Ts), S0=[s($id, {$src[]})|Stk] :- int($id) | Ret = suc(R, Stk, Exp, p($id, {$src[]}), Map, Ss, Ts), Exp = state_space.react_nd_set(Rs, {$src[]}, R).

exp_@@Ret = exp({$rs[], @rs}, [], Map, Ss, Ts), ini(I) :- Ret = state_space(I, Map, Ss, Ts).

suc@@Ret = suc(Rs, Stk, [{$dest[]}|Suc], Src, Map, Ss, Ts) :- M = state_space.state_map_find(Map, {$dest[]}, ID), Ret = ns0(Rs, Stk, Suc, Src, p(ID, {$dest[]}), M, Ss, Ts).

suc_@@Ret = suc(Rs, Stk, [], p($id, {$src[]}), Map, Ss, Ts) :- int($id) | Ret = exp(Rs, Stk, Map, Ss, Ts).

ns0@@Ret = ns0(Rs, Stk, Suc, Src, p($d, D), Map, Ss, Ts) :- int($d) | Ret = ns(Rs, Stk, Suc, Res, Src, p($d, D), Map, S, Ts), S = set.find(Ss, $d, Res).

ns@@Ret = ns(Rs, Stk, Suc, some, p($s, Src), p($d, Dst), Map, Ss, Ts) :- int($s), int($d) | Ret = nt(Rs, Stk, Suc, Res, p($s, Src), p($d, Dst), Map, Ss, T), T = set.find(Ts, '.'($s, $d), Res).

ns_@@Ret = ns(Rs, Stk, Suc, none, p($s, Src), p($d, Dst), Map, Ss, Ts), n($n), t($t) :- int($s), int($d), $nn=$n+1, $tt=$t+1| Ret = suc(Rs, [s($d, Dst)|Stk], Suc, p($s, Src), Map, S, T), S = set.insert(Ss, $d), T = set.insert(Ts, '.'($s, $d)), n($nn), t($tt).

nt@@Ret = nt(Rs, Stk, Suc, some, Src, p($d, {$dest[]}), Map, Ss, Ts) :- int($d) | Ret = suc(Rs, Stk, Suc, Src, Map, Ss, Ts).

nt_@@Ret = nt(Rs, Stk, Suc, none, p($s, Src), p(D, {$dest[]}), Map, Ss, Ts), t($t) :- int($s), $tt=$t+1 | Ret = suc(Rs, Stk, Suc, p($s, Src), Map, Ss, set.insert(Ts, '.'($s, D))), t($tt).

Ret = state_space(I, M, S, T) :- Ret = ss(I, M, set.to_list(S), set.to_list(T)). Ret = ss(I, M, [$x|S], T) :- int($x) | Ret = ss(I, state_space.state_map_find(M, $x, Res), S, T),state($x, Res).

- 実行オプション
` slim --hl --use-builtin-rule code.lmn`
- 出力結果
-- `!!`の状態は本来`3`の状態と同型

set.use. state_space.use. n(7). t(11). ret(ss(140583858388368,,[],[[140583858411520|140583858415488],[140583858349888|140583858413056],[140583858409440|140583858411520],[140583858368272|140583858413056],[140583858409440|140583858349888],[140583858368272|140583858415488],[140583858388368|140583858409440],[140583858409440|140583858368272],[140583858349888|140583858388368],[140583858413056|140583858409440],[140583858411520|140583858413056]])).

1::state(140583858388368,{p_thinking(L25,fork_free(L26)). p_thinking(L26,fork_free(L27)). p_thinking(L27,fork_free(L25)). }). @41. @43. @56. 2::state(140583858409440,{p_thinking(L16,fork_free(L17)). p_thinking(L17,fork_free(L18)). p_one_fork(L18,fork_used(L16)). }). 3::state(140583858411520,{p_thinking(L19,fork_free(L20)). p_one_fork(L21,fork_used(L19)). p_one_fork(L20,fork_used(L21)). }). 4::state(140583858349888,{p_thinking(L22,fork_used(L23)). p_thinking(L24,fork_free(L22)). fork_used(L24,p_eating(L23)). }). !!::state(140583858368272,{p_thinking(L7,fork_free(L8)). p_one_fork(L8,fork_used(L9)). p_one_fork(L9,fork_used(L7)). }). 5::state(140583858413056,{p_thinking(L10,fork_used(L11)). p_one_fork(L12,fork_used(L10)). fork_used(L12,p_eating(L11)). }). 6::state(140583858415488,{p_one_fork(L13,fork_used(L14)). p_one_fork(L14,fork_used(L15)). p_one_fork(L15,fork_used(L13)). }).


- slimで実行するコード

p_t(L0, R0), f_f(L0, R1). p_t(L1, R1), f_f(L1, R2). p_t(L2, R2), f_f(L2, R0).

p_t(L0, R0), f_f(L1, R0) :- p_o(L0, R0), f_u(L1, R0). p_o(L0, R0), f_u(L1, R0), f_f(L0, R1) :- p_e(L2, R2), f_u(L1, R2), f_u(L2, R1). p_e(L0, R0), f_u(L0, R1), f_u(L1, R0) :- p_t(L2, R2), f_f(L2, R1), f_f(L1, R2).

- 実行オプション
` slim --nd -t code.lmn`
- 出力結果

States 1::{p_t(L0,f_f(L1)). p_t(L1,f_f(L2)). p_t(L2,f_f(L0)). @4. } 2::{p_t(L0,f_f(L1)). p_t(L1,f_f(L2)). p_o(L2,f_u(L0)). @4. } 3::{p_t(L0,f_f(L1)). p_o(L2,f_u(L0)). p_o(L1,f_u(L2)). @4. } 4::{p_t(L0,f_u(L1)). p_t(L2,f_f(L0)). f_u(L2,p_e(L1)). @4. } 5::{p_t(L0,f_u(L1)). p_o(L2,f_u(L0)). f_u(L2,p_e(L1)). @4. } 6::{p_o(L0,f_u(L1)). p_o(L1,f_u(L2)). p_o(L2,f_u(L0)). @4. }

Transitions init:1 1::2 2::3,4 3::6,5 4::5,1 5::2 6::

'# of States'(stored) = 6. '# of States'(end) = 1.

lmntal / slim

メタインタプリタの状態数バグ #255