Mercurial > hg > Applications > Lite
changeset 15:816425e04ea7
fix true - omega interval satisfiability
| author | kono |
|---|---|
| date | Sat, 20 Jan 2001 21:21:44 +0900 |
| parents | 0d896bcc1061 |
| children | 4360c2030303 |
| files | ex.pl infinite.pl problems |
| diffstat | 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. - setof(S,(links(S,1),integer(S)),Children), + setof(S,links(S,1),Children), 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) :- - setof(S,(links(S,H),integer(S)),Children), + setof(S,links(S,H),Children), 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 - setof(S,(links(S,H),integer(S)),Children), + 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 - setof(S,(links(S,H),integer(S)),Children), + 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),integer(S)),Children), + 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).