% Addition to the DMC system to check liveness properties and
% to measure running times in milliseconds.
% Maurizio Proietti Nov 21, 2007

ln:- liveness_nw.     %no widening
lw:- liveness_aw.     %with accurate widening on outer least fixpoint


liveness_nw:-		%liveness without widening
    clearC,
    clearTempVerify,
    liveness_nw(prop(outer),prop(inner)). 

liveness_aw:-		%liveness with accurate widening on outer least fixpoint
    clearC,
    clearTempVerify,
    liveness_aw(prop(outer),prop(inner)). 

liveness_nw(F1,F2):-        
 clearZ,
 clearS,
 parse_assert(gfp,F2),
 gfp1(n,NoSteps),!,
 turn_zero(NoSteps),
 clearZ,
 clearC,
 parse_assert(gfp,F1),
 intersect_db,
 lfp(n),!.

liveness_aw(F1,F2):-
 clearZ,
 clearS,
 parse_assert(gfp,F2),
 gfp1(n,NoSteps),!,
 turn_zero(NoSteps),
 clearZ,
 clearC,
 parse_assert(gfp,F1),
 intersect_db,
 lfp(aw),!.


gfp1(Mode,K):-
 template(T),
 assert(s(0,T,{},0,(0,0))),
 gfixpoint(Mode,0,1,K). 
% time(gfixpoint(Mode,0,1,K),_Time,_,_,_).  


time_ms(Goal,T,M,P,C):-			%running time of Goal in milliseconds
        statistics(runtime,[T1,_]),
        Goal,
        statistics(runtime,[T2,_]),
        statistics(memory,[M,_]),
        statistics(program,[P,_]),
        statistics(choice,[C,_]),
        T is T2-T1.

% printtime(G) G is a goal
%

ptime_ms(G):-				%running time of goal G in milliseconds
  time_ms(G,T,_,_,_),
  nl,
  write('Execution time '),
  write(T), 
  write(ms).