:- dynamic testsetBase/1.
%:- use_module(library(random)).
%:- use_module(library(lists)).
%:- use_module(library(system)).
:- consult(simplify).

:- op(900,fy,not).

%simplifyOpt(no).
simplifyOpt(yes).
%simplifications([cutOnProp(r1)]).
%simplifications([flatten]).
simplifications([]).
orderingOpt(normal).
sortOpt([negateProp(r1)]).
%sortOpt([disjunction]).
sortOpt([]).

toPLpltl(and(Conjuncts0),and(Conjuncts1)) :-
	toPLconj(Conjuncts0,Conjuncts1).
toPLconj([],[]) :-
	!.
toPLconj([always(or(C1))|CL1],CL2) :-
	toPLconj(CL1,CL3),
	(member(sometime(_),C1) ->
	    CL2 = CL3
	;
	    toPLdisj(C1,CL4),
	    append(CL3,CL4,CL2)
	).
toPLconj([or(C1)|CL1],CL2) :-
	toPLconj(CL1,CL3),
	toPLdisj(C1,CL4),
	append(CL3,CL4,CL2).
toPLdisj(Disj,CL) :-
	splitdisj(Disj,D2,D3),
	(D2 == [] ->
	    toxpropClause(D3,DX3),
	    CL = [or(D3),or(DX3)]
	;
	    (D3 == [] ->
		toxpropClause(D2,DX2),
		CL = [or(DX2)]
	    ;
		gensym(r,R),
		toxpropClause(D3,DX3),
		toxpropClause(D2,DX2),
		CL = [or([not(R)|D3]),or([not(R)|DX3]),or([R|DX2])]
	    )
	),
	!.

splitdisj([],[],[]) :-
	!.
splitdisj([L|D1],D2,D3) :-
	splitdisj(D1,ND2,ND3),
	(L = next(M) ->
	    D2 = [M|ND2],
	    D3 = ND3
	;
	    D2 = ND2,
	    D3 = [L|ND3]
	),
	!.

toxpropClause([],[]) :-
	!.
toxpropClause([L1|CL1],[L2|CL2]) :-
	toxprop(L1,L2),
	toxpropClause(CL1,CL2).

toxprop(L1,L2) :-
	(L1 = not(M1) ->
	    atom_chars(M1,MChars),
	    atom_chars(M2,[120|MChars]),
	    L2 = not(M2)
	;
	    atom_chars(L1,MChars),
	    atom_chars(L2,[120|MChars])
	).

%------------------------------------------------------------
strippltl(and(Conjuncts0),and(Conjuncts1)) :-
	stripconj(Conjuncts0,Conjuncts1).
stripconj([],[]) :-
	!.
stripconj([always(or(C1))|CL1],CL2) :-
	stripconj(CL1,CL3),
	(member(sometime(_),C1) ->
	    CL2 = CL3
	;
	    stripdisj(C1,C2),
	    CL2 = [or(C2)|CL3]
	).
stripdisj([],[]) :-
	!.
stripdisj([next(L1)|DL1],[L1|DL2]) :-
	stripdisj(DL1,DL2).


%------------------------------------------------------------	    
	    

genpltl(N,K,L,and(Formula),and(Formula3)) :-
	getProblemSeries(SN),
	(SN == x ->
	    genpltl0(N,K,L,Formula1,Formula3),
	    gendiamonds0(N,Formula2),
	    append(Formula1,Formula2,Formula)
	;
	    (SN == y ->
		genpltl1(N,K,L,Formula1),
		genloop1(N,N,N,StepClauses),
		gendiamonds1(N,Formula2),
		append(Formula1,StepClauses,Formula0),
		number_chars(N,NChars),
		atom_chars(A1,[113|NChars]),
		append(Formula0,[or([not(r1),q1]),or([not(r1),not(A1)])|Formula2],Formula)
	    ;
		genpltl2(N,K,L,Formula1),
		genother1(0,N,Disj),
		Formula = [or(Disj)|Formula1]
	    )
	).

genpltl0(N,K,L,[always(or(Seq1))|Formula0],[or(Seq2)|Formula1]) :-
	(L > 1 ->
	    M is L-1,
	    genpltl0(N,K,M,Formula0,Formula1)
	;
	    Formula0 = [],
	    Formula1 = []
	),
	randseq0(K,N,Seq0),
	gendisj0(Seq0,Seq1,Seq2).

randseq0(K,N,[R|Seq0]) :-
	(N < K ->
	    !, fail
	;
	    (K > 1 ->
		L is K-1,
		randseq0(L,N,Seq0)
	    ;
		Seq0 = []
	    ),
	    newrandom(N,Seq0,R)
	),
	!.
newrandom(N,Seq,R) :-
	Try is random(N)+1,
	(member(Try,Seq) ->
	    newrandom(N,Seq,R)
	;
	    R = Try
	),
	!.

gendisj0([],[],[]) :-
	!.
gendisj0([N1|NL],[L1|LL],[L2|LL2]) :-
	number_chars(N1,N1Chars),
	atom_chars(A1,[112|N1Chars]),
	R is random(2),
	(R < 1 ->
	    L1 = next(not(A1)),
	    L2 = not(A1)
	;
	    L1 = next(A1),
	    L2 = A1
	),
	gendisj0(NL,LL,LL2),
	!.

gendiamonds0(N,Formula) :-
	gendiamonds0(1,N,Formula).

gendiamonds0(I,N,[always(or([not(A1),sometime(A2)]))|Formula0]) :-
	number_chars(I,IChars),
	Iplus is I+1,
	(Iplus > N ->
	    J = 1,
	    Formula0 = []
	;
	    J = Iplus,
	    gendiamonds0(J,N,Formula0)
	),
	number_chars(J,JChars),
	atom_chars(A1,[112|IChars]),
	atom_chars(A2,[112|JChars]),
	!.

genpltl1(N,K,L,Formula1) :-
	(L > 1 ->
	    M is L-1,
	    genpltl1(N,K,M,Formula0)
	;
	    Formula0 = []
	),
	randseq0(K,N,Seq0),
%	gendisj0(Seq0,Seq1,_Seq2),
%	genclauses2(1,N,Seq1,Clauses1),
	gendisj1(Seq0,Seq1,_Seq2),
	genclauses3(1,N,Seq1,Clauses1),
	append(Clauses1,Formula0,Formula1).


genpltl2(N,K,L,Formula1) :-
	(L > 1 ->
	    M is L-1,
	    genpltl2(N,K,M,Formula0)
	;
	    Formula0 = []
	),
	randseq0(K,N,Seq0),
	gendisj0(Seq0,Seq1,_Seq2),
	genclauses4(N,N,Seq1,Clauses1),
	append(Clauses1,Formula0,Formula1).



genstep1(1,A,[always(or([not(A),next(not(q1))]))]) :-
	!.
genstep1(N,A,[always(or([not(A),next(not(A1))]))|StepClauses]) :-
	number_chars(N,NChars),
	atom_chars(A1,[113|NChars]),
	StepClauses = [].
%	M is N-1,
%	genstep1(M,A,StepClauses).

genloop1(N,N,N,[always(or([not(A1),next(r1)]))|StepClauses]) :-
	number_chars(N,NChars),
	atom_chars(A1,[114|NChars]),
	M is N-1,
	genstep1(N,A1,StepClauses1),
	genloop1(M,N,N,StepClauses2),
	append(StepClauses1,StepClauses2,StepClauses),
	!.
genloop1(K,M,N,[always(or([not(A1),next(A2)]))|StepClauses]) :-
	number_chars(K,KChars),
	atom_chars(A1,[114|KChars]),
	number_chars(M,MChars),
	atom_chars(A2,[114|MChars]),
	genstep1(N,A1,StepClauses1),
	L is K-1,
	(L < 1 ->
	    StepClauses2 = []
	;
	    genloop1(L,K,N,StepClauses2)
	),
	append(StepClauses1,StepClauses2,StepClauses),
	!.

genclauses1(0,_N,_,[]) :-
	!.
genclauses1(M,N,Seq1,[always(or([next(not(A1))|Seq1]))|Clauses1]) :-
	number_chars(M,NChars),
	atom_chars(A1,[113|NChars]),
	K is M-1,
	genclauses1(K,N,Seq1,Clauses1).


genclauses2(0,_N,_,[]) :-
	!.
genclauses2(M,N,Seq1,[always(or([A1|Seq1]))|Clauses1]) :-
	number_chars(M,NChars),
	atom_chars(A1,[114|NChars]),
	K is M-1,
	genclauses2(K,N,Seq1,Clauses1).

genclauses3(0,_N,_,[]) :-
	!.
genclauses3(M,N,Seq1,[or([A1|Seq1])|Clauses1]) :-
	number_chars(M,NChars),
	atom_chars(A1,[114|NChars]),
	K is M-1,
	genclauses3(K,N,Seq1,Clauses1).

genclauses4(0,_N,_,[]) :-
	!.
genclauses4(M,N,Seq1,[always(or(Seq2))|Clauses1]) :-
	number_chars(M,NChars),
	atom_chars(A1,[114|NChars]),
	K is M-1,
	append(Seq1,[A1],Seq2),
	genclauses4(K,N,Seq1,Clauses1).

genother(N,N,[]) :-
	!.
genother(M,N,[next(A1)|Literals]) :-
%	N>M,
	number_chars(N,NChars),
	atom_chars(A1,[113|NChars]),
	K is N-1,
	genother(M,K,Literals).


genother1(N,N,[]) :-
	!.
genother1(M,N,[not(A1)|Literals]) :-
%	N>M,
	number_chars(N,NChars),
	atom_chars(A1,[114|NChars]),
	K is N-1,
	genother1(M,K,Literals).
	

randseq1(K,N,[R|Seq0]) :-
	(N < K ->
	    !, fail
	;
	    (K > 1 ->
		L is K-1,
		randseq1(L,N,Seq0)
	    ;
		Seq0 = []
	    ),
	    newrandom(N,Seq0,R)
	),
	!.

gendisj1([],[],[]) :-
	!.
gendisj1([N1|NL],[L1|LL],[L2|LL2]) :-
	number_chars(N1,N1Chars),
	atom_chars(A1,[112|N1Chars]),
	R is random(2),
	(R < 1 ->
	    L1 = not(A1),
	    L2 = not(A1)
	;
	    L1 = A1,
	    L2 = A1
	),
	gendisj1(NL,LL,LL2),
	!.

gendiamonds1(N,Formula) :-
	gendiamonds1(1,N,Formula).

gendiamonds1(I,N,[always(or([not(A1),sometime(A2)])),always(or([not(A2),A3|OtherLiterals]))|Formula0]) :-
	number_chars(I,IChars),
	atom_chars(A1,[113|IChars]),
	J is I+1,
	number_chars(J,JChars),
	atom_chars(A2,[115|JChars]),
	atom_chars(A3,[113|JChars]),
	genother(J,N,OtherLiterals),
	(J >= N ->
	    Formula0 = []
	;
	    gendiamonds1(J,N,Formula0)
	),
	!.


%---------------------------------------------------------------------------
% printFormulaLWB(+TERM)
% print term TERM using the LWB syntax for modal formulae.
% The syntax of the output conforms with the input syntax of the logic
% workbench.
%
printFormulaLWB(sometime(C)) :-
	write('F('),
	printFormulaLWB(C),
	write(')').
printFormulaLWB(always(C)) :-
	write('G('),
	printFormulaLWB(C),
	write(')').
printFormulaLWB(next(C)) :-
	write('X('),
	printFormulaLWB(C),
	write(')').
printFormulaLWB(and(L)) :-
	write('('),
	printFormulasLWB(' and ',L),
	write(')').
printFormulaLWB(or(L)) :-
	write('('),
	printFormulasLWB(' or ',L),
	write(')').
printFormulaLWB(not(A)) :-
	write('not( '),
	printFormulaLWB(A),
	write(')').
printFormulaLWB(A) :-
	atomic(A),
	write(A).
printFormulasLWB(_Op,[T1]) :-
	printFormulaLWB(T1).
printFormulasLWB(Op,[T1,T2|TL]) :-
	printFormulaLWB(T1),
	write(' '),
	write(Op),
	write(' '),
	printFormulasLWB(Op,[T2|TL]).

%---------------------------------------------------------------------------
% printFormulaSpin(+TERM)
% print term TERM using the Spin syntax for modal formulae.
% The syntax of the output conforms with the input syntax of the logic
% workbench.
%
printFormulaSpin(sometime(C)) :-
	write('<>('),
	printFormulaSpin(C),
	write(')').
printFormulaSpin(always(C)) :-
	write('[]('),
	printFormulaSpin(C),
	write(')').
printFormulaSpin(next(C)) :-
	write('X('),
	printFormulaSpin(C),
	write(')').
printFormulaSpin(and(L)) :-
	write('('),
	printFormulasSpin(' && ',L),
	write(')').
printFormulaSpin(or(L)) :-
	write('('),
	printFormulasSpin(' || ',L),
	write(')').
printFormulaSpin(not(A)) :-
	write('!( '),
	printFormulaSpin(A),
	write(')').
printFormulaSpin(A) :-
	atomic(A),
	write(A).
printFormulasSpin(_Op,[T1]) :-
	printFormulaSpin(T1).
printFormulasSpin(Op,[T1,T2|TL]) :-
	printFormulaSpin(T1),
	write(' '),
	write(Op),
	write(' '),
	printFormulasSpin(Op,[T2|TL]).

%---------------------------------------------------------------------------
% printFormulaStep(+TERM)
% print term TERM using the Step syntax for modal formulae.
% The syntax of the output conforms with the input syntax of the logic
% workbench.
%
printFormulaStep(F) :-
	write('SPEC'), nl,
	getSignature(F,Sig),
	printVarDecl(Sig), nl,
	write('PROPERTY example : '),
	write('!('),
	printGoalStep(F), 
	write(')'), nl.

printVarDecl([]) :-
	!.
printVarDecl([V|VL]) :-
	write('variable '),
	printVarDecl1([V|VL]),
	write(': bool Flexible').

printVarDecl1([]) :-
	!.
printVarDecl1([V]) :-
	write(V).
printVarDecl1([V1,V2|VL]) :-
	write(V1),
	write(', '),
	printVarDecl1([V2|VL]).

printGoalStep(sometime(C)) :-
	write('<>('),
	printGoalStep(C),
	write(')').
printGoalStep(always(C)) :-
	write('[]('),
	printGoalStep(C),
	write(')').
printGoalStep(next(C)) :-
	write('()('),
	printGoalStep(C),
	write(')').
printGoalStep(and(L)) :-
	write('('),
	printFormulasStep(' /\\ ',L),
	write(')').
printGoalStep(or(L)) :-
	write('('),
	printFormulasStep(' \\/ ',L),
	write(')').
printGoalStep(not(A)) :-
	write('!( '),
	printGoalStep(A),
	write(')').
printGoalStep(A) :-
	atomic(A),
	write(A).
printFormulasStep(_Op,[T1]) :-
	printGoalStep(T1).
printFormulasStep(Op,[T1,T2|TL]) :-
	printGoalStep(T1),
	write(' '),
	write(Op),
	write(' '),
	printFormulasStep(Op,[T2|TL]).

getSignature([],[]) :-
        !.
getSignature(Term,[Term]) :-
        atomic(Term),
        !.
getSignature(Term,Sig) :-
        Term =.. [_|Terms],
        getSignatures(Terms,Sig).
getSignatures([],[]).
getSignatures([T1|TL1],Sig) :-
        getSignature(T1,Sig1),
        getSignatures(TL1,Sig2),
        oset_union(Sig1,Sig2,Sig).

%---------------------------------------------------------------------------
% printFormulaMONA(+TERM)
% print term TERM using the MONA syntax for WS1S formulae.
%

printFormulaMONA(F) :-
	write('var1 b,e;'),nl,
	getSignature(F,Sig),
	printVarDeclMONA(Sig), nl, nl,
	write('#next predicate'), nl,
	write('pred next(var1 x, var1 y) = '), nl,
        write('     (((x < e) & (y = x + 1)) | ((x = e) & (y = b + 1)));'),nl,
	write('#connect predicate'), nl,
	write('pred conn(var1 x, var1 y) = '), nl,
	write('(ex2 S: (x in S & y in S & '), nl,
	write('         (all1 y1: (all1 z1: ((y1 in S & next(y1,z1)) => z1 in S))) &'),nl,
 	write('         (all2 T: ((x in T & '),nl,
        write('                   (all1 y2: (all1 z2: ((y2 in T & next(y2,z2)) => z2 in T)))) '),
        write(' => (S sub T)))));'), nl,
	printFormMONA(F,0), write(';'), nl,
	!.

printVarDeclMONA([]) :-
	!.
printVarDeclMONA([V|VL]) :-
	write('var2 '),
	printVarDeclMONA1([V|VL]),
	write(';').

printVarDeclMONA1([]) :-
	!.
printVarDeclMONA1([V]) :-
	write(V).
printVarDeclMONA1([V1,V2|VL]) :-
	write(V1),
	write(', '),
	printVarDeclMONA1([V2|VL]).

printFormMONA(always(C),X) :-
	gensym(x,Y),
	format("(all1 ~a: (conn(~a,~a) => ",[Y,X,Y]),
	printFormMONA(C,Y),
	format("))~n",[]).
printFormMONA(sometime(C),X) :-
	gensym(x,Y),
	format("(ex1 ~a: (conn(~a,~a) & ",[Y,X,Y]),
	printFormMONA(C,Y),
	format("))",[]).
printFormMONA(next(C),X) :-
	gensym(x,Y),
	format("(ex1 ~a: (next(~a,~a) & ",[Y,X,Y]),
	printFormMONA(C,Y),
	format("))",[]).
printFormMONA(and(L),X) :-
	write('('),
	printFormsMONA(' & ',L,X),
	write(')').
printFormMONA(or(L),X) :-
	write('('),
	printFormsMONA(' | ',L,X),
	write(')').
printFormMONA(not(A),X) :-
	write('~( '),
	printFormMONA(A,X),
	write(')').
printFormMONA(A,X) :-
	format("(~a in ~a)",[X,A]).
printFormsMONA(_Op,[T1],X) :-
	printFormMONA(T1,X).
printFormsMONA(Op,[T1,T2|TL],X) :-
	printFormMONA(T1,X),
	write(' '),
	write(Op),
	write(' '),
	printFormsMONA(Op,[T2|TL],X).

%---------------------------------------------------------------------------
% printFormulaPTLJava(alc2tltool,+TERM)
% print term TERM using the LWB syntax for modal formulae.
% The syntax of the output conforms with the input syntax of the logic
% workbench.
%
printFormulaPTLJava(sometime(C)) :-
	write('F('),
	printFormulaPTLJava(C),
	write(')').
printFormulaPTLJava(always(C)) :-
	write('(G('),
	printFormulaPTLJava(C),
	write('))').
printFormulaPTLJava(next(C)) :-
	write('X('),
	printFormulaPTLJava(C),
	write(')').
printFormulaPTLJava(and(L)) :-
	write('('),
	printFormulasPTLJava(' & ',L),
	write(')').
printFormulaPTLJava(or(L)) :-
	write('('),
	printFormulasPTLJava(' | ',L),
	write(')').
printFormulaPTLJava(not(A)) :-
	write('~( '),
	printFormulaPTLJava(A),
	write(')').
printFormulaPTLJava(A) :-
	atomic(A),
	write(A).
printFormulasPTLJava(_Op,[T1]) :-
	printFormulaPTLJava(T1).
printFormulasPTLJava(Op,[T1,T2|TL]) :-
	printFormulaPTLJava(T1),
	write(' '),
	write(Op),
	write(' '),
	printFormulasPTLJava(Op,[T2|TL]).

%---------------------------------------------------------------------------
% printFormulaSNF(+TERM)
% print term TERM using the LWB syntax for modal formulae.
% The syntax of the output conforms with the input syntax of the logic
% workbench.
%
printFormulaSNF(F) :-
	write('wlast imp '),
	printFormulaTRTP(F).
printFormulaTRTP(sometime(C)) :-
	write('sometime('),
	printFormulaTRTP(C),
	write(')').
printFormulaTRTP(always(C)) :-
	write('always('),
	printFormulaTRTP(C),
	write(')').
printFormulaTRTP(next(C)) :-
	write('next('),
	printFormulaTRTP(C),
	write(')').
printFormulaTRTP(and(L)) :-
	write('('),
	printFormulasTRTP(' and ',L),
	write(')').
printFormulaTRTP(or(L)) :-
	write('('),
	printFormulasTRTP(' or ',L),
	write(')').
printFormulaTRTP(not(A)) :-
	write('not( '),
	printFormulaTRTP(A),
	write(')').
printFormulaTRTP(A) :-
	atomic(A),
	write(A).
printFormulasTRTP(_Op,[T1]) :-
	printFormulaTRTP(T1).
printFormulasTRTP(Op,[T1,T2|TL]) :-
	printFormulaTRTP(T1),
	write(' '),
	write(Op),
	write(' '),
	printFormulasTRTP(Op,[T2|TL]).

%---------------------------------------------------------------------------
% printFormulaDLP(alc2dlp,+TERM)
% print term TERM using the LWB syntax for modal formulae.
% The syntax of the output conforms with the input syntax of the logic
% workbench.
%
printFormulaDLP(sometime(C)) :-
	write('(SOME (TRANSITIVE r1) '),
	printFormulaDLP(C),
	write(')').
printFormulaDLP(always(C)) :-
	write('(ALL (TRANSITIVE r1) '),
	printFormulaDLP(C),
	write(')').
printFormulaDLP(next(C)) :-
	write('(ALL r1 '),
	printFormulaDLP(C),
	write(')').
printFormulaDLP(and(L)) :-
	write('(AND '),
	printFormulasDLP('',L),
	write(')').
printFormulaDLP(or(L)) :-
	write('(OR '),
	printFormulasDLP('',L),
	write(')').
printFormulaDLP(not(A)) :-
	write('(NOT '),
	printFormulaDLP(A),
	write(')').
printFormulaDLP(A) :-
	atomic(A),
	write(A).
printFormulasDLP(_Op,[T1]) :-
	printFormulaDLP(T1).
printFormulasDLP(Op,[T1,T2|TL]) :-
	printFormulaDLP(T1),
	write(' '),
	write(Op),
	write(' '),
	printFormulasDLP(Op,[T2|TL]).

%---------------------------------------------------------------------------
% printFormulaClatter(+TERM)
% print term TERM using the LWB syntax for modal formulae.
% The syntax of the output conforms with the input syntax of the logic
% workbench.
%
printFormulaClatter([C1,C2|CL]) :-
	printFormulaClatter(C1),
	write(';'), nl,
	printFormulaClatter([C2|CL]).
printFormulaClatter([C1]) :-
	printFormulaClatter(C1),
	write('.'), nl,
	write('.'), nl.
printFormulaClatter(implies(A,S)) :-
	printFormulaClatter(A),
	write(' => '),
	printFormulaClatter(S).
printFormulaClatter(start) :-
	write('Q false'),
	!.
printFormulaClatter(true) :-
	write('true'),
	!.
printFormulaClatter(previous(C)) :-
	write('Y '),
	printFormulaClatter(C),
	!.
printFormulaClatter(sometime(C)) :-
	write('F('),
	printFormulaClatter(C),
	write(')').
printFormulaClatter(always(C)) :-
	write('G('),
	printFormulaClatter(C),
	write(')').
printFormulaClatter(next(C)) :-
	write('X('),
	printFormulaClatter(C),
	write(')').
printFormulaClatter(and(L)) :-
	write('('),
	printFormulasClatter(' & ',L),
	write(')').
printFormulaClatter(or(L)) :-
	write('('),
	printFormulasClatter(' | ',L),
	write(')').
printFormulaClatter(not(A)) :-
	write('~'),
	printFormulaClatter(A).
printFormulaClatter(A) :-
	atomic(A),
	write(A).
printFormulasClatter(_Op,[T1]) :-
	printFormulaClatter(T1).
printFormulasClatter(Op,[T1,T2|TL]) :-
	printFormulaClatter(T1),
	write(' '),
	write(Op),
	write(' '),
	printFormulasClatter(Op,[T2|TL]).

toClatter(and(C),D) :-
	toClatter(C,D).
toClatter([],[]) :-
	!.
toClatter([C1|CL1],CL2) :-
	toClatterClause(C1,CL3),
	toClatter(CL1,CL4),
	append(CL3,CL4,CL2).

toClatterClause(always(or(C)),DL) :-
	(member(sometime(L),C) ->
	    toClatterSometime(L,C,DL)
	;
	    toClatterStep(C,DL)
	).
	    
toClatterSometime(L,C,D) :-
	getNonSometime(C,E,F),
	gensym(s,S),
	D = [implies(previous(and([not(L)|E])),sometime(L)),
             implies(start,or([S,L|F])),
	     implies(start,or([not(L),S])),
	     implies(previous(true),or([not(L),S])),
             implies(previous(and([not(S)])),sometime(L))].
toClatterStep(C,D) :-
	splitdisj(C,NextLits,NormalLits),
	negatedisj(NormalLits,NegatedLits),
	(NegatedLits = [] ->
	    D = [implies(previous(true),or(NextLits))]
	;
	    D = []
	).

negatedisj([],[]) :-
	!.
negatedisj([not(L)|C],[L|D]) :-
	!,
	negatedisj(C,D).
negatedisj([L|C],[not(L),D]) :-
	negatedisj(C,D).


getNonSometime([],[],[]) :-
	!.
getNonSometime([sometime(_)|C],D,E) :-
	!,
	getNonSometime(C,D,E).
getNonSometime([not(L)|C],[L|D],[not(L)|E]) :-
	!,
	getNonSometime(C,D,E).
getNonSometime([L|C],[not(L)|D],[L|E]) :-
	getNonSometime(C,D,E).
	    

testSAT(lwb,VN,AN,ON) :-
	generateFilename('/var/tmp/script/','_lwb.in',VN,0,AN,ON,0,0,LWB_Input_File),
	generateFilename('/var/tmp/script/','_lwb.out',VN,0,AN,ON,0,0,LWB_Output_File),
	genpltl(VN,ON,AN,Term,PropTerm),
	tell(LWB_Input_File),
	write('load(pltl);'),
	nl,
	write('ct := clockticks();'),
	nl,
	write('print("Satisfiable PLTL-formula: ");'),
	nl,
	write('satisfiable('),
	printFormulaLWB(Term),
	write(');'),
	nl,
	write('ct :== (clockticks()-ct) mult 10;'),
	nl,
	write('print("Runtime PLTL-formula: ",ct," milliseconds");'),
	nl,
	write('ct :== clockticks();'),
	nl,
	write('print("Satisfiable PL-formula:   ");'),
	nl,
	write('satisfiable('),
	printFormulaLWB(PropTerm),
	write(');'),
	nl,
	write('ct :== (clockticks()-ct) mult 10;'),
	nl,
	write('print("Runtime PL-formula:   ",ct," milliseconds");'),
	nl,
	write('quit;'),
	nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0]),
	format("using - module PLTL of the logic workbench (version 1.0)~n",[]),
	format("writing protocol to ~a.~n",[LWB_Output_File]),
	ttyflush,
	!,
	systemCall(exec,['nice -19 /usr/local/lwb-1.1/bin/lwb < ',LWB_Input_File,' > ',LWB_Output_File,' 2>&1']),
	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush.

testSAT(tempRes,VN,AN,ON,Random) :-
	getProblemSeries(SN),
	tell('/var/tmp/tempRes.pl'),
	format(":- assert(testseries(~a)).~n",[SN]),
	format(":- testSAT(temporalResolution,~d,~d,~d,~d).~n",[VN,AN,ON,Random]),
	format(":- halt.~n",[]),
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - temporal resolution (version 1.0)~n",[]),
	ttyflush,
	systemCall(exec,['sicstus -r /home/staff1/lect/ullrich/provers/PLTLresolution/TRP -l /var/tmp/tempRes.pl']),
	ttyflush.
testSAT(trp,VN,AN,ON,Random) :-
	getProblemSeries(SN),
	tell('/var/tmp/tempRes.pl'),
	format(":- assert(testseries(~a)).~n",[SN]),
	format(":- testSAT(temporalResolution,~d,~d,~d,~d).~n",[VN,AN,ON,Random]),
	format(":- halt.~n",[]),
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - temporal resolution (version 1.0)~n",[]),
	ttyflush,
	systemCall(exec,['/users/lect/ullrich/provers/TRP-SWI/TRP']),
	ttyflush.
testSAT(trtp,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	generateFilename('/var/tmp/trtp','.in',VN,0,AN,ON,0,Random,Input_File),
	generateFilename('/var/tmp/trtp','.out',VN,0,AN,ON,0,Random,_Output_File),
	tell(Input_File),
	write('otres(['),
	printFormulaSNF(Term),
	write(']).'), nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - TRTP (version 1.0)~n",[]),
	ttyflush,
	!.
testSAT(lwb11sat,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	generateFilename('/var/tmp/script','_lwb.in',VN,0,AN,ON,0,Random,LWB_Input_File),
	generateFilename('/var/tmp/script','_lwb.out',VN,0,AN,ON,0,Random,LWB_Output_File),
	pltlSimplification(Term,Term3),
	tell(LWB_Input_File),
	write('load(pltl);'), nl,
	write('print("Provability of negated PLTL-formula: ");'), nl,
	write('ct :== clockticks();'), nl,
	write('provable(~('),
	printFormulaLWB(Term3),
	write('));'), nl,
	write('ct :== (clockticks()-ct) mult 10;'), nl,
	write('print("Runtime PLTL-formula: ",ct," milliseconds");'), nl,
	write('quit;'),	nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - the `provable' function of module PLTL of the Logics Workbench (version 1.1)~n",[]),
	format("writing protocol to ~a.~n",[LWB_Output_File]),
	ttyflush,
	!,
	systemCall(exec,['ulimit -t 1100; nice -19 /usr/local/lwb-1.1/bin/lwb < ',LWB_Input_File,' > ',LWB_Output_File,' 2>&1']),
	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush.
testSAT(lwb11model,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	generateFilename('/var/tmp/script','_lwb.in',VN,0,AN,ON,0,Random,LWB_Input_File),
	generateFilename('/var/tmp/script','_lwb.out',VN,0,AN,ON,0,Random,LWB_Output_File),
	pltlSimplification(Term,Term3),
	tell(LWB_Input_File),
	write('load(pltl);'), nl,
	write('ct :== clockticks();'), nl,
	write('print("Satisfiable PLTL-formula: ");'), nl,
	write('m :== model('),
	printFormulaLWB(Term3),
	write(');'), nl,
	write('ct :== (clockticks()-ct) mult 10;'), nl,
	write('if (m = false) then false; else true;'), nl,
	write('print(m);'), nl,
	write('print("Runtime PLTL-formula: ",ct," milliseconds");'), nl,
	write('quit;'),	nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - the `model' function of module PLTL of the Logics Workbench (version 1.1)~n",[]),
	format("writing protocol to ~a.~n",[LWB_Output_File]),
	ttyflush,
	!,
	systemCall(exec,['ulimit -t 1100; nice -19 /usr/local/lwb-1.1/bin/lwb < ',LWB_Input_File,' > ',LWB_Output_File,' 2>&1']),
	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush.
testSAT(lwb10,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	generateFilename('/var/tmp/script','_lwb.in',VN,0,AN,ON,0,Random,LWB_Input_File),
	generateFilename('/var/tmp/script','_lwb.out',VN,0,AN,ON,0,Random,LWB_Output_File),
	pltlSimplification(Term,Term3),
	tell(LWB_Input_File),
	write('load(pltl);'), nl,
	write('ct :== clockticks();'), nl,
	write('print("Satisfiable PLTL-formula: ");'), nl,
	write('satisfiable('),
	printFormulaLWB(Term3),
	write(');'), nl,
	write('ct :== (clockticks()-ct) mult 10;'), nl,
	write('print("Runtime PLTL-formula: ",ct," milliseconds");'), nl,
	write('quit;'),	nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - the `satisfiable' function of module PLTL of the Logic Workbench (version 1.0)~n",[]),
	format("writing protocol to ~a.~n",[LWB_Output_File]),
	ttyflush,
	!,
	systemCall(exec,['ulimit -t 1100; nice -19 /usr/local/lwb-1.1/bin/lwb < ',LWB_Input_File,' > ',LWB_Output_File,' 2>&1']),
	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush.
testSAT(clatter,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	generateFilename('/var/tmp/clatter','_tres.in',VN,0,AN,ON,0,Random,LWB_Input_File),
	generateFilename('/var/tmp/clatter','_tres.out',VN,0,AN,ON,0,Random,LWB_Output_File),
	toClatter(Term,ClatterClauses),
	tell(LWB_Input_File),
	printFormulaClatter(ClatterClauses),
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - Clatter-2001~n",[]),
	format("writing protocol to ~a.~n",[LWB_Output_File]),
	ttyflush,
	!,
	systemCall(exec,['cd /home/staff2/prof/michael/Clatter-2001; nice -19 /usr/bin/time -f "%Uuser %Ssystem %ewall %Mmem" ./clatter -d /tmp/clatter.process < ',LWB_Input_File,' > ',LWB_Output_File,' 2>&1']),
	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush.
testSAT(dlp,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	(simplifyOpt(yes) ->
	    simplify_pltl(Term,Term2)
	;
	    Term2 = Term
	),  
	Input_File = '/var/tmp/dlp.in',
        Output_File = '/var/tmp/dlp.out',
	tell(Input_File),
	Clauses is AN+VN+1,
	format("#CL: ~d ~d ~d #IT: ~d #var: ~d MPI TEST~n",[VN,ON,2,1,VN]),
	format("~d CLAUSES~n",[Clauses]),
	write('(AND (ALL (TRANSITIVE r1) (SOME r1 (OR p0 (NOT p0))))'), nl,
	printFormulaDLP(Term2),
	write(')'), nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - DLP 4.1~n",[]),
	format("writing protocol to ~a.~n",[Output_File]),
	ttyflush,
	!,
	systemCall(exec,['cd /users/lect/ullrich/provers/DLP-4.1/ps; nice -19 ./RunK']),
	systemCall(system,['cat ',Output_File]),
	ttyflush.
testSAT(dlps,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	Input_File = '/var/tmp/dlp.in',
        Output_File = '/var/tmp/dlp.out',
	tell(Input_File),
	Clauses is AN+VN+1,
	format("#CL: ~d ~d ~d #IT: ~d #var: ~d MPI TEST~n",[VN,ON,2,1,VN]),
	format("~d CLAUSES~n",[Clauses]),
	write('(AND (ALL (TRANSITIVE r1) (SOME r1 (OR p0 (NOT p0))))'), nl,
	printFormulaDLP(Term),
	write(')'), nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - DLP 4.1~n",[]),
	format("writing protocol to ~a.~n",[Output_File]),
	ttyflush,
	!,
	systemCall(exec,['cd /users/lect/ullrich/provers/DLP-4.1/ps; nice -19 ./RunK']),
	systemCall(system,['cat ',Output_File]),
	ttyflush.
testSAT(lwbpl,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	generateFilename('/var/tmp/script','_lwb.in',VN,0,AN,ON,0,Random,LWB_Input_File),
	generateFilename('/var/tmp/script','_lwb.out',VN,0,AN,ON,0,Random,LWB_Output_File),
	strippltl(Term,PropTerm),
	tell(LWB_Input_File),
	write('load(pltl);'), nl,
	write('ct := clockticks();'), nl,
	generateTests(VN,PropTerm),
        write('ct := (clockticks()-ct) mult 10;'), nl,
	write('print("Runtime PLTL-formula: ",ct," milliseconds");'), nl,
	write('quit;'),	nl,
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - module PLTL of the logic workbench (version 1.0)~n",[]),
	format("writing protocol to ~a.~n",[LWB_Output_File]),
	ttyflush,
	!,
	systemCall(exec,['ulimit -t 1100; nice -19 /usr/local/lwb-1.1/bin/lwb < ',LWB_Input_File,' > ',LWB_Output_File,' 2>&1']),
	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush,
	format("Finished random example: ~d-~d-~d-~d-~d-~d.~n~n",[VN,0,AN,ON,0,Random]),
	ttyflush.
testSAT(mona,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	pltlSimplification(Term,Term3),
	generateFilename('/var/tmp/mona','.in',VN,0,AN,ON,0,Random,MONA_Input_File),
	generateFilename('/var/tmp/mona','.out',VN,0,AN,ON,0,Random,MONA_Output_File),
	tell(MONA_Input_File),
	printFormulaMONA(Term3),
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - MONA 1.4~n",[]),
	format("writing protocol to ~a.~n",[MONA_Output_File]),
	ttyflush,
	!,
	graciousCall(exec,['ulimit -t 1100; /usr/bin/time -f "%Uuser %Ssystem %ewall %Mmem" /usr/local/mona-1.4/mona -q -t ',MONA_Input_File,' > ',MONA_Output_File,' 2>&1']),
	systemCall(system,['cat ',MONA_Output_File]),
	ttyflush.
testSAT(spin,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	pltlSimplification(Term,Term3),
	generateFilename('/var/tmp/spin','.in',VN,0,AN,ON,0,Random,Spin_Input_File),
	generateFilename('/var/tmp/spin','.out',VN,0,AN,ON,0,Random,Spin_Output_File),
	tell(Spin_Input_File),
	printFormulaSpin(Term3),
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - Spin 3.4.8~n",[]),
	format("writing protocol to ~a.~n",[Spin_Output_File]),
	ttyflush,
	!,
%	systemCall(exec,['cd /users/lect/ullrich/provers/Spin; nice -19 ./spin -F ',Spin_Input_File,' > ',LWB_Output_File,' 2>&1']),
%	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush.
testSAT(step,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	pltlSimplification(Term,Term3),
	generateFilename('/var/tmp/step','.in',VN,0,AN,ON,0,Random,Step_Input_File),
	generateFilename('/var/tmp/step','.out',VN,0,AN,ON,0,Random,Step_Output_File),
	tell(Step_Input_File),
	printFormulaStep(Term3),
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - Step 1.4~n",[]),
	format("writing protocol to ~a.~n",[Step_Output_File]),
	ttyflush,
	!,
	graciousCall(exec,['/usr/bin/time -f "%Uuser %Ssystem %ewall %Mmem" /usr/local/bin/STeP -ptl ',Step_Input_File,' -exit > ',Step_Output_File,' 2>&1']),
	systemCall(system,['cat ',Step_Output_File]),
	ttyflush.
testSAT(tltool,VN,AN,ON,Random) :-
	generateSourceFilename(VN,0,AN,ON,0,Random,File),
	see(File),
	read(Term),
	seen,
	Input_File = '/var/tmp/tltool.in',
        Output_File = '/var/tmp/tltool.out',
	(simplifyOpt(yes) ->
	    simplify_pltl(Term,Term1),
	    (orderingOpt(reverse) ->
		(Term1 = and(L) ->
		    reverse(L,L2),
		    Term3 = and(L2)
		;
		    Term3 = Term1
		)
	    ;
		Term3 = Term1
	    )
	;
	    Term3 = Term
	),
	tell(Input_File),
	printFormulaPTLJava(not(Term3)),
	told,
	format("Starting random example: ~d-~d-~d-~d-~d-~d.~n",[VN,0,AN,ON,0,Random]),
	format("using - the TempLogic tool~n",[]),
	format("writing protocol to ~a.~n",[Output_File]),
	ttyflush,
	!,
	systemCall(exec,['cd /users/lect/ullrich/provers/PTLJava; nice -19 /usr/local/jdk1.2.2/bin/java TempLogic/TLTool']),
	systemCall(system,['cat ',Output_File]),
	ttyflush.

generateTests(N1,and(L)) :-
	generateTests0(N1,and(L)),
	generateTests1(N1,and(L)).

generateTests0(N1,and(L)) :-
	createNegConj(N1,C),
	write('print("Satisfiable PL-formula for '),
	write(C), 
	write(': ");'), nl,
	write('satisfiable('),
	append(C,L,L1),
	printFormulaLWB(and(L1)),
	write(');'), nl,
	!.

createNegConj(N1,C2) :-
	(N1 > 0 ->
	    number_chars(N1,N1Chars),
	    atom_chars(A1,[112|N1Chars]),
	    M is N1-1,
	    createNegConj(M,C1),
	    C2 = [not(A1)|C1]
	;
	    C2 = []
	),
	!.	

generateTests1(N1,and(L)) :-
	(N1 > 0 ->
	    number_chars(N1,N1Chars),
	    atom_chars(A1,[112|N1Chars]),
	    write('print("Satisfiable PL-formula for '),
	    write(A1), 
	    write(': ");'), nl,
	    write('satisfiable('),
	    printFormulaLWB(and([A1|L])),
	    write(');'), nl,
	    M is N1-1,
	    generateTests1(M,and(L))
	;
	    true
	),
	!.


getProverDir(D) :-
	(file_exists('/users/lect/ullrich/provers') ->
	    D = '/users/lect/ullrich/provers'
	;
	    D = '/HG/opt/provers'
	).
%getProblemBase(D) :-
%	testsetBase(D),
%	!.
getProblemBase('/users/lect/ullrich/provers/experiments/pltl/samples/') :-
	!.

getProblemSeries(D) :-
	testseries(D),
	!.
getProblemSeries(x) :-
	!.


% generateFilename(+BASE,+SUFFIX,+VN,+RN,+AN,+ON,+GR,+LB,-File)
% Erzeugt einen Filenamen nach folgender Methode:
% Der Filename beginnt mit BASE gefolgt von den Parametern VN, RN, AN, ON, GR und 
% LB jeweils durch einen Bindestrich getrennt, gefolgt von SUFFIX.


generateSourceFilename(VN,RN,AN,ON,GR,RandomNumber,File) :-
	getProblemBase(BASE),
	getProblemSeries(SN),
	generateAtom([BASE,'pltl-',VN,'-',RN,'-',SN,'-',ON,'-',GR,'/pltl-',VN,'-',RN,'-',AN,'-',ON,'-',GR,'-',RandomNumber,'.prolog.concept'],[],File).

generateFilename(BASE,SUFFIX,VN,RN,AN,ON,GR,RandomNumber,File) :-
	generateAtom([BASE,'-',VN,'-',RN,'-',AN,'-',ON,'-',GR,'-',RandomNumber,SUFFIX],[],File).

generateAtom([],AtomString,Atom) :-
	atom_chars(Atom,AtomString).
generateAtom([A|L],AtomString1,Atom) :-
	(number(A) ->
	    number_chars(A,AC)
	;
	    (atomic(A) ->
		atom_chars(A,AC)
	    ;
		AC = A
	    )
	),
	append(AtomString1,AC,AtomString2),
	generateAtom(L,AtomString2,Atom).

graciousCall(CallPredicate,Command) :-
	once(systemCall(Command,[],CallPredicate)),
	!.
graciousCall(_,_) :-
	!.

systemCall(CallPredicate,Command) :-
	once(systemCall(Command,[],CallPredicate)),
	!.
systemCall(_CallPredicate,Command) :-
	write('SystemCall of '),
	write(Command),
	write(' failed.'),
	nl,
	!.

systemCall([],CommandString,_) :-
	atom_chars(Command,CommandString),
	!,
	shell(Command).
systemCall([],CommandString,shell(Result)) :-
	atom_chars(Command,CommandString),
	!,
	shell(Command,Result).
systemCall([A|L],CommandString1,CallPredicate) :-
	(number(A) ->
	    number_chars(A,AC)
	;
	    (atomic(A) ->
		atom_chars(A,AC)
	    ;
		AC = A
	    )
	),
	append(CommandString1,AC,CommandString2),
	systemCall(L,CommandString2,CallPredicate).

genSAT(VN,AN,ON) :-
	genSAT(99,VN,AN,ON).
genSAT(N,VN,AN,ON) :-
	(N >= 0 ->
	    Random is 200000+N,
	    generateSourceFilename(VN,0,AN,ON,0,Random,File),
	    genpltl(VN,ON,AN,PLTL,_PL),
	    tell(File),
	    write(PLTL),
	    write('.'),
	    nl,
	    told,
	    M is N-1,
	    genSAT(M,VN,AN,ON)
	;
	    true
	),
	!.

pltlSimplification(Term,Term3) :-
	(simplifyOpt(yes) ->
	    simplify_pltl(Term,Term1)
	;
	    Term1 = Term
	),
	(orderingOpt(reverse) ->
	    (Term1 = and(L) ->
		reverse(L,L2),
		Term3 = and(L2)
	    ;
		(Term1 = or([and([C1,and(L1)]),and([C2,and(L2)])]) ->
		    reverse([C1|L1],RL1),
		    reverse([C2|L2],RL2),
		    Term3 = or([and(RL1),and(RL2)])
		;
		    (Term1 = or([and(L1),and(L2)]) ->
			reverse(L1,RL1),
			reverse(L2,RL2),
			Term3 = or([and(RL1),and(RL2)])
		    ;
			Term3 = Term1
		    )
		)
	    )
	;
	    Term3 = Term1
	),
	!.

testSATSeq(Prover,VN,AN,ON) :-
	testSATNum(0,100,Prover,VN,AN,ON).
testSATNum(N,Max,Prover,VN,AN,ON) :-
	(N < Max ->
	    Random is N+200000,
	    testSAT(Prover,VN,AN,ON,Random),
	    M is N+1,
	    testSATNum(M,Max,Prover,VN,AN,ON)
	;
	    true
	),
	!.

testFile(dlp,File) :-
        VN = 10, ON = 10, AN = 10,
	see(File),
	read(Term),
	seen,
	pltlSimplification(Term,Term2),
	Input_File = '/var/tmp/dlp.in',
        Output_File = '/var/tmp/dlp.out',
	tell(Input_File),
	Clauses is AN+VN+1,
	format("#CL: ~d ~d ~d #IT: ~d #var: ~d MPI TEST~n",[VN,ON,2,1,VN]),
	format("~d CLAUSES~n",[Clauses]),
	write('(AND (ALL (TRANSITIVE r1) (SOME r1 (OR p0 (NOT p0))))'), nl,
	printFormulaDLP(Term2),
	write(')'), nl,
	told,
	format("Starting computation~n",[]),
	format("using - DLP 4.1~n",[]),
	format("writing protocol to ~a.~n",[Output_File]),
	ttyflush,
	!,
	systemCall(exec,['cd /users/lect/ullrich/provers/DLP-4.1/ps; nice -19 ./RunK']),
	systemCall(system,['cat ',Output_File]),
	ttyflush.
testFile(lwb,File) :-
        VN = 10, ON = 10, AN = 10,
	see(File),
	read(Term),
	seen,
	pltlSimplification(Term,Term2),
	generateFilename('/var/tmp/file','_lwb.in',VN,0,AN,ON,0,0,LWB_Input_File),
	generateFilename('/var/tmp/file','_lwb.out',VN,0,AN,ON,0,0,LWB_Output_File),
	tell(LWB_Input_File),
	write('load(pltl);'),
	nl,
	write('ct := clockticks();'),
	nl,
	write('print("Satisfiable PLTL-formula: ");'),
	nl,
	write('satisfiable('),
	printFormulaLWB(Term2),
	write(');'),
	nl,
	write('ct := (clockticks()-ct) mult 10;'),
	nl,
	write('print("Runtime PLTL-formula: ",ct," milliseconds");'),
	nl,
	write('quit;'),
	nl,
	told,
	format("Starting computation~n",[]),
	format("using - module PLTL of the logic workbench (version 1.0)~n",[]),
	format("writing protocol to ~a.~n",[LWB_Output_File]),
	ttyflush,
	!,
	systemCall(exec,['nice -19 /usr/local/lwb-1.1/bin/lwb < ',LWB_Input_File,' > ',LWB_Output_File,' 2>&1']),
	systemCall(system,['cat ',LWB_Output_File]),
	ttyflush.

% The following assertion fixes the `type' of benchmark
% formulae that will be generated. Possible values are
% 'x' and 'y'.
testseries(y).
:- simplifyOpt(X), format("simplifyOpt(~p)~n",[X]).
:- simplifications(X), format("simplifications(~p)~n",[X]).
:- orderingOpt(X), format("orderingOpt(~p)~n",[X]).
:- sortOpt(X), format("sortOpt(~p)~n",[X]).
:- systemCall(system,['hostname']).
% The following is an sample call of the random generator
% It generates formulae with 12 propositional variables,
% 5 clauses (well, how many clauses actually depends on
% the type of the benchmark formulae that will be generated),
% and three literals per clause.
%:- genSAT(12,5,3), halt.