# HG changeset patch
# User kono
# Date 980005870 -32400
# Node ID 4360c203030387468bd86b6d7084dbbde77f09d5
# Parent  816425e04ea7714039ae5660ce7a89bc99fba119
strange...

diff -r 816425e04ea7 -r 4360c2030303 ex.pl
--- a/ex.pl	Sat Jan 20 21:21:44 2001 +0900
+++ b/ex.pl	Sun Jan 21 00:51:10 2001 +0900
@@ -260,7 +260,12 @@
 ex(402,*skip).
 ex(403,*length(5)).
 ex(404,~('<>'(empty))).
-ex(405,('<>'(empty))).
+ex(405,('<>'(empty))).   % unsatisfiable 
 ex(406,(infinite-> @infinite)).
+ex(407,((less(5),[](q))&(length(3)&([](<>(p)),[](<>(~p)),*length(6))))).
+ex(408,(infinite -> ~(<>([](p)) = [](<>(p))))).  % satisfiable
+ex(409,finite).   % unsatisfiable
+
+
 
 /* end */
diff -r 816425e04ea7 -r 4360c2030303 infinite.pl
--- a/infinite.pl	Sat Jan 20 21:21:44 2001 +0900
+++ b/infinite.pl	Sun Jan 21 00:51:10 2001 +0900
@@ -37,8 +37,21 @@
     make_hist([L,L],L1),
     write_ce(L1,0),nl.
 write_infinite_seq1(L) :-
-    make_hist(L,L1),
-    write_ce(L1,0),nl.
+    insert_loop_mark(L,L1),
+    make_hist(L1,L2),
+    write_ce(L2,0),nl.
+
+insert_loop_mark(L,L1) :-
+    last(L,Last),
+    insert_loop_mark(L,Last,L1).
+
+last([Last],Last) :-!.
+last([_|T],Last) :-
+    last(T,Last).
+
+insert_loop_mark([Last|T],Last,[(*),Last|T]):-!.
+insert_loop_mark([H|T],Last,[H|T1]):-
+    insert_loop_mark(T,Last,T1).
 
 retract_all(X) :-
     retract(X),fail.
@@ -47,62 +60,61 @@
 infinite(L) :-
     % 1 seems like original ITL formula that is root.
     setof(S,links(S,1),Children),
-    more_only_node(1,Children,L,[],[1]).
+    more_node(1,Children,L,[],[1]).
 infinite([]) :-
     found_infinite.
 
-% more_only(S) :- 
-%     state(S,[empty|_],true),!,fail.
-% more_only(S) :- number(S).
+infinite_node(S) :- 
+     state(S,[empty|_],true),!,fail.
+infinite_node(S) :- number(S).
 
-more_only(true) :- !.
-more_only(S) :- 
-    number(S),
-    state(S,[more|_],_).
+%infinite_node(true) :- !.
+%infinite_node(S) :- 
+%    number(S),
+%    state(S,[more|_],_).
 
-more_only_node(S,[S1|Children],[S|L],L1,Hist) :-
+more_node(S,[S1|Children],[S|L],L1,Hist) :-
 %    write('checking '),write(S),nl,
-    more_only(S),
+    infinite_node(S),
     % starting false loop
-    more_only_loop(S1,Children,L,L1,[S|Hist],[S]).
-more_only_node(S,Children,L,L1,Hist) :- % goto one depth deeper
-    more_only_node1(Children,L,L1,[S|Hist]).
+    more_loop(S1,Children,L,L1,[S|Hist],[S]).
+more_node(S,Children,L,L1,Hist) :- 
+    % goto one depth deeper
+    more_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_node1([H|_],L,L1,Hist) :-
+    not_member(H,Hist),
     setof(S,links(S,H),Children),
-    more_only_node(H,Children,L,L1,Hist).
-more_only_node1([_|T],L,L1,Hist) :-
-    more_only_node1(T,L,L1,Hist).
+    more_node(H,Children,L,L1,Hist).
+more_node1([_|T],L,L1,Hist) :-
+    more_node1(T,L,L1,Hist).
 
-more_only_loop(true,_,[true|L],L,_Hist,_Seq) :-
+more_loop(true,_,[true|L],L,_Hist,_Seq) :-
     assert(found_infinite).
-more_only_loop(S,_,[S|L],L,_Hist,Seq) :-
+more_loop(S,_,[S|L],L,_Hist,Seq) :-
     member(S,Seq),!,
     assert(found_infinite).
     % we find the one
-more_only_loop(S,_,L,L,Hist,_Seq) :-
+more_loop(S,_,L,L,Hist,_Seq) :-
     member(S,Hist),!,
     fail.	
     % end of this branch
-more_only_loop(H,_,[H|L],L1,Hist,Seq) :-
-    more_only(H),!,		
+more_loop(H,_,[H|L],L1,Hist,Seq) :-
+    infinite_node(H),!,		
     % still in the false interval
     setof(S,links(S,H),Children),
-    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
+    more_loop1(Children,L,L1,[H|Hist],[H|Seq]).
+more_loop(_,[S|T],L,L1,Hist,Seq) :-!,
+    % try another child
+    more_loop(S,T,L,L1,Hist,Seq).
+% more_loop(H,[],L,L1,Hist,Seq) :-!,fail.
+    % empty case. fail and try another branch
+
+
+more_loop1([H|_],L,L1,Hist,Seq) :-
     setof(S,links(S,H),Children),
-    % we already know S i not more_only
-    more_only_node1(Children,L,L1,[H|Hist]).
-
-more_only_loop1([H|_],L,L1,Hist,Seq) :-
-    setof(S,links(S,H),Children),
-    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).
+    more_loop(H,Children,L,L1,Hist,Seq).
+more_loop1([_|T],L,L1,Hist,Seq) :-
+    more_loop1(T,L,L1,Hist,Seq).
 
 /* end */
diff -r 816425e04ea7 -r 4360c2030303 problems
--- a/problems	Sat Jan 20 21:21:44 2001 +0900
+++ b/problems	Sun Jan 21 00:51:10 2001 +0900
@@ -1,8 +1,39 @@
+Sun Jan 21 00:42:39 JST 2001
+
+あれ? やっぱり、なんか変だな。
+    | ?- ex(finite & empty).
+
+    state(1 , not(true&false)&empty)
+    [][empty]->empty
+    [][more]->1
+
+    0.019000000000005457 sec.
+    1 states
+    2 subterms
+    2 state transions
+    verbose,renaming,singleton,length limit 5
+    valid
+
+    yes
+    | ?- infinite.
+    satisfiable in infinite interval:
+    *
+    0:      1
+では、困ります。それに、
+    <>(p) = finite & p
+に書き換えないといけないみたいね。
+
+ってことは、やはり、
+    その状態から、唯一、more にだけ抜ける状態
+なのかな。
+
 Sat Jan 20 20:50:17 JST 2001
 
 true をloopとみなしてないので、ex(true) で、infinite 
 が satisfiable にならない。
 
+infinite で、loop を * で明示するようにした。
+
 Sat Jan 20 18:16:33 JST 2001
 
 とりあえず、more_only は、more にいくものが何かあれば許すと言うことに
diff -r 816425e04ea7 -r 4360c2030303 read.me
--- a/read.me	Sat Jan 20 21:21:44 2001 +0900
+++ b/read.me	Sun Jan 21 00:51:10 2001 +0900
@@ -82,6 +82,11 @@
     but it only shows one possible state transition conditon for a
     state transition.
 
+?-infinite. 
+      Check satisfiability on infinite interval. Like exe, it shows
+      possible accept states with a loop marked by *. To check infinite
+      validity, use negation.
+
     In case of a large formula, you may want to make output tarse.
 
 ?-verbose(off). 
@@ -186,6 +191,9 @@
     gets(A,B)	=   keep(@A<->B)
     stable(A) 	=   keep(@A<->A)
 
+    infinite    =   (true&false)
+    finite      =   ~infinite
+
     P proj Q  	=   Q is true using P as a clock period
     *P          =   P&P&..&P.. chop infinite closure