# HG changeset patch
# User kono
# Date 979913640 -32400
# Node ID f2aa38ce07875cc4d87011a1fdab6785128cf990
# Parent  95897517e4642c7bd88dc923d30569b93fd62888
add state display.

diff -r 95897517e464 -r f2aa38ce0787 Makefile
--- a/Makefile	Fri Jan 19 20:37:32 2001 +0900
+++ b/Makefile	Fri Jan 19 23:14:00 2001 +0900
@@ -35,7 +35,7 @@
 
 all:    $(PROLOG_TYPE)
 
-SICSTUS: cp.pl
+SICSTUS: cp.pl 
 	echo '[initm],save(lite).' | $(PROLOG)
 CPROLOG: cp.pl
 	echo '[init],save(lite).' | $(PROLOG)
@@ -60,7 +60,7 @@
 
 .SUFFIXES: .pl .ql
 .SILENT:
-OBJ = op.ql ndcomp.ql dvcomp.ql bdtstd.ql rstd.ql chop.ql diag.ql kiss.ql ex.ql cp.ql
+OBJ = op.ql ndcomp.ql dvcomp.ql bdtstd.ql rstd.ql chop.ql diag.ql kiss.ql ex.ql cp.ql infinite.ql
 # kiss_ex.ql
 WORK = .tmpl .tmpc .tmpa .tmpb
 # M = lite:
diff -r 95897517e464 -r f2aa38ce0787 diag.pl
--- a/diag.pl	Fri Jan 19 20:37:32 2001 +0900
+++ b/diag.pl	Fri Jan 19 23:14:00 2001 +0900
@@ -87,6 +87,10 @@
 	make_hist0(L,P,C).
 
 make_hist0([],_,[]):-!.
+make_hist0([D|L],*,[*|L1]):-!, 
+	make_hist0(L,D,L1).
+make_hist0([*|L],S,[*|L1]):-!, 
+	make_hist0(L,S,L1).
 make_hist0([D|L],S,[(D->Cond)|L1]):-!,  % step by step
 	state(S,Cond,D),
 	!,  				% 
@@ -95,6 +99,8 @@
 % trace 2variable renamings
 
 make_hist1([],_,_,R,R,[]):-!.
+make_hist1([*|L],S,P,R,R1,[*|L1]):-!,  
+	make_hist1(L,S,P,R,R1,L1).
 make_hist1([SN|L],S,P,R,R1,[(SN->Cond)|L1]):-!,  % step by step
 	state(S,Cond,SN,P,P1,R,R0),
 	!,
@@ -120,6 +126,9 @@
 write_diag(counter_example(Hist)) :-!,write_ce(Hist,0).
 write_diag(execution(Hist)) :-!,write_ce(Hist,0).
 	write_ce([],_):-!.
+	write_ce([(*)|T],I) :- !,
+	    write(*),nl,
+	    write_ce(T,I).
 	write_ce([(S->[E|L])|T],I) :- (E=more,L=L1;E=empty,L=L1;[E|L]=L1),!,
 		write(I),write(:),write_cond(L1),put(9),write(S),nl,
 		J is I+1,
diff -r 95897517e464 -r f2aa38ce0787 infinite.pl
--- a/infinite.pl	Fri Jan 19 20:37:32 2001 +0900
+++ b/infinite.pl	Fri Jan 19 23:14:00 2001 +0900
@@ -31,8 +31,9 @@
     write('unsatisfiable in infinite interval.'),nl.
 
 write_infinite_seq(L) :-
-    write('satisfiable in infinite interval: '),
-    write(L),nl.
+    write('satisfiable in infinite interval:'),nl,
+    make_hist(L,L1),
+    write_ce(L1,0),nl.
 
 retract_all(X) :-
     retract(X),fail.
@@ -50,6 +51,7 @@
 
 more_only_node(S,[S1|Children],[S|L],L1,Hist) :-
     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).
@@ -84,6 +86,6 @@
     setof(S,(links(S,H),integer(S)),Children),
     more_only_loop(H,Children,L,L1,Hist,Seq).
 more_only_loop1([_|T],L,L1,Hist,Seq) :-
-    more_only_loop(T,L,L1,Hist,Seq).
+    more_only_loop1(T,L,L1,Hist,Seq).
 
 /* end */
diff -r 95897517e464 -r f2aa38ce0787 initm
--- a/initm	Fri Jan 19 20:37:32 2001 +0900
+++ b/initm	Fri Jan 19 23:14:00 2001 +0900
@@ -7,6 +7,10 @@
 % ?-op(60,fy,['~','#','<>', '@',^]).
 % ?-op(60,fy,[*]).
 
+:- use_module(library(system)).
+
+unix(system(X)) :- system(X).
+
 :-lite:[op].
 
 :-
diff -r 95897517e464 -r f2aa38ce0787 lite.pl
--- a/lite.pl	Fri Jan 19 20:37:32 2001 +0900
+++ b/lite.pl	Fri Jan 19 23:14:00 2001 +0900
@@ -34,7 +34,7 @@
 %?-op(60,fy,[*]).
 ?-[op].
 % :- use_module(library(gmlib)).
-:- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp]).
+:- ensure_loaded([dvcomp,rstd,chop,diag,kiss,ex,cp,infinite]).
 % ,display]).
 
 % end
diff -r 95897517e464 -r f2aa38ce0787 problems
--- a/problems	Fri Jan 19 20:37:32 2001 +0900
+++ b/problems	Fri Jan 19 23:14:00 2001 +0900
@@ -1,3 +1,44 @@
+Fri Jan 19 20:59:46 JST 2001
+
+    | ?- ex((infinite -> @infinite)).
+
+    state(1 , not(true&false),@ (true&false))
+    [][empty]->empty
+    [][more]->true
+
+    0.021000000000000796 sec.
+    1 states
+    2 subterms
+    2 state transions
+    verbose,renaming,singleton,length limit 5
+    valid
+
+    yes
+    | ?- infinite.
+    unsatisfiable in infinite interval.
+
+これは... どういうことなんでしょうね? inifite は基本的に
+false だから、inifite-> タイプのものは、すべて、infinite unsatisfiable
+だね。
+
+Fri Jan 19 20:40:37 JST 2001
+
+割りと簡単なアルゴリズムで、satisfiabilityは、チェック
+できました。これが、正しいかどうかは Moszkowski によるけど...
+   inifnite
+   *skip
+   *((skip&skip))
+などに関しては、うまく動くようですね。
+
+vailidity checker が欲しい所だけど... どういうものがvalidなのかは、
+良くわからない。もちろん、否定が unsatisfiable ならば、valid なの
+だが。
+
+でも、この方法だと、
+    satisfiable in ω-interval implies
+      falsifiable in finite interval
+ってことになるらしい。
+
 Fri Jan 19 07:48:59 JST 2001
 
 Streett     ∩_i []<>L_i ⊃ <>[]U _i