### changeset 15:816425e04ea7

fix true - omega interval satisfiability
author kono Sat, 20 Jan 2001 21:21:44 +0900 0d896bcc1061 4360c2030303 ex.pl infinite.pl problems 3 files changed, 25 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
```--- a/ex.pl	Sat Jan 20 20:47:00 2001 +0900
+++ b/ex.pl	Sat Jan 20 21:21:44 2001 +0900
@@ -259,6 +259,8 @@
ex(401,*infinite).
ex(402,*skip).
ex(403,*length(5)).
-ex(403,~('<>'(empty))).
+ex(404,~('<>'(empty))).
+ex(405,('<>'(empty))).
+ex(406,(infinite-> @infinite)).

/* end */```
```--- a/infinite.pl	Sat Jan 20 20:47:00 2001 +0900
+++ b/infinite.pl	Sat Jan 20 21:21:44 2001 +0900
@@ -10,7 +10,7 @@

Infinite satisfiability/validity checker

-A set of non-empty-exit looping states represents infinite
+A set of `more' looping states represents infinite
interval in ITL. The loop can contains deterministic state
choice. This should correspond Rabin/Strreet Automaton
that is non-deterministic Buchi automaton.
@@ -46,7 +46,7 @@

infinite(L) :-
% 1 seems like original ITL formula that is root.
more_only_node(1,Children,L,[],[1]).
infinite([]) :-
found_infinite.
@@ -55,24 +55,31 @@
%     state(S,[empty|_],true),!,fail.
% more_only(S) :- number(S).

+more_only(true) :- !.
more_only(S) :-
number(S),
state(S,[more|_],_).

more_only_node(S,[S1|Children],[S|L],L1,Hist) :-
%    write('checking '),write(S),nl,
-    more_only(S),!,
+    more_only(S),
% starting false loop
more_only_loop(S1,Children,L,L1,[S|Hist],[S]).
-more_only_node(_,Children,L,L1,Hist) :- % goto one depth deeper
-    more_only_node1(Children,L,L1,Hist).
+more_only_node(S,Children,L,L1,Hist) :- % goto one depth deeper
+    more_only_node1(Children,L,L1,[S|Hist]).

+more_only_node1([H|_],_L,_L1,Hist) :-
+    member(H,Hist),
+    !,
+    fail.
more_only_node1([H|_],L,L1,Hist) :-
more_only_node(H,Children,L,L1,Hist).
more_only_node1([_|T],L,L1,Hist) :-
-    more_only_node(T,L,L1,Hist).
+    more_only_node1(T,L,L1,Hist).

+more_only_loop(true,_,[true|L],L,_Hist,_Seq) :-
+    assert(found_infinite).
more_only_loop(S,_,[S|L],L,_Hist,Seq) :-
member(S,Seq),!,
assert(found_infinite).
@@ -84,16 +91,16 @@
more_only_loop(H,_,[H|L],L1,Hist,Seq) :-
more_only(H),!,
% still in the false interval
more_only_loop1(Children,L,L1,[H|Hist],[H|Seq]).
more_only_loop(H,[S|_],[H|L],L1,Hist,_) :-
% false interval ends, start new search in depth first way
% we already know S i not more_only
more_only_node1(Children,L,L1,[H|Hist]).

more_only_loop1([H|_],L,L1,Hist,Seq) :-
more_only_loop(H,Children,L,L1,Hist,Seq).
more_only_loop1([_|T],L,L1,Hist,Seq) :-
more_only_loop1(T,L,L1,Hist,Seq).```
```--- a/problems	Sat Jan 20 20:47:00 2001 +0900
+++ b/problems	Sat Jan 20 21:21:44 2001 +0900
@@ -1,3 +1,8 @@
+Sat Jan 20 20:50:17 JST 2001
+
+true をloopとみなしてないので、ex(true) で、infinite
+が satisfiable にならない。
+
Sat Jan 20 18:16:33 JST 2001

とりあえず、more_only は、more にいくものが何かあれば許すと言うことに```