1		:- module(logging,[synthesis_log/1,disable_logging/0,enable_logging/0]).
2
3		:- use_module(probsrc(translate),[print_bexpr/1,print_bexpr_or_subst/1]).
4
5		:- use_module(library(lists)).
6
7		:- dynamic enabled/1.
8		:- volatile enabled/1.
9
10		enabled(false).
11
12		disable_logging :-
13		retractall(enabled(_)) ,
14		assert(enabled(false)).
15
16		enable_logging :-
17		retractall(enabled(_)) ,
18		assert(enabled(true)).
19
20		synthesis_log(LoggingPredicate) :-
21		(enabled(true) ; LoggingPredicate =.. [solution|_]) ,
22		synthesis_log_aux(LoggingPredicate) , !.
23		synthesis_log(_) :- !.
24
25		synthesis_log_aux(solution_tuple(ProgramAST1,ProgramAST2)) :-
26		format("~nFound two eventually equivalent solutions:~n~w~n",[ProgramAST1]) ,
27		nl , print_bexpr_or_subst(ProgramAST1) , nl ,
28		print_bexpr_or_subst(ProgramAST2) , nl.
29
30		synthesis_log_aux(solution(_,none)) :-
31		format("~nSynthesis failed.~n",[]).
32		synthesis_log_aux(solution(_,state(State))) :-
33		format("~nDistinguishing State: ~w~n",[State]).
34		synthesis_log_aux(solution(_,transition(InputState,OutputState))) :-
35		format("~nDistinguishing Transition: ~w --> ~w~n",[InputState,OutputState]).
36		synthesis_log_aux(solution(Type,Solution)) :-
37		synthesis_log_aux(solution_enter(Type)) ,
38		synthesis_log_aux(solution_aux1(Type,Solution)).
39		% Solution can be a list of actions.
40		synthesis_log_aux(solution_aux1(action,Action)) :-
41		\+is_list(Action) , ! ,
42		synthesis_log_aux(solution_aux2(action,[Action])).
43		synthesis_log_aux(solution_aux1(action,Actions)) :-
44		synthesis_log_aux(solution_aux2(action,Actions)).
45		synthesis_log_aux(solution_aux1(Type,Solution)) :-
46		Type \= action ,
47		print_bexpr_or_subst(Solution) , nl.
48		synthesis_log_aux(solution_aux2(action,[])).
49		synthesis_log_aux(solution_aux2(action,[Action|T])) :-
50		print_bexpr_or_subst(Action) , nl ,
51		synthesis_log_aux(solution_aux2(action,T)).
52
53		synthesis_log_aux(solution_enter(Type)) :-
54		(Type = action -> PrintType = operation ; PrintType = Type) ,
55		format("~nSynthesized ~w:~n",[PrintType]).
56
57		synthesis_log_aux(symmetry_reduction(SymmetryReduction)) :-
58		format("~nSymmetry reduction:~n",[]) ,
59		print_bexpr(SymmetryReduction) , nl.
60
61		synthesis_log_aux(relax_guard(OpName)) :-
62		format("~nStart synthesizing relaxed guard for operation ~w ~n",[OpName]).
63
64		synthesis_log_aux(invariant_violation_initialisation_state(Init)) :-
65		format("~nInvariant violation in initialisation state ~w",[Init]).
66
67		synthesis_log_aux(invariant_violation_found(State,Operation)) :-
68		format("~nInvariant violation in state ~w, caused by operation ~w ~n",[State,Operation]).
69
70		synthesis_log_aux(involved_variables(VarNames)) :-
71		format("~nVariables involved in invariant violation: ~w.~n",[VarNames]).
72
73		synthesis_log_aux(synthesize_new_guard_if_loop) :-
74		format("~nSynthesize new precondition for an operation that fits the current example.~n",[]).
75
76		synthesis_log_aux(distinguishing_constraint(Type,Constraint)) :-
77		format("~nDistinguishing constraint for type ~w:~n",[Type]) ,
78		print_bexpr(Constraint) , nl.
79
80		synthesis_log_aux(distinguishing_transition_cache_changed(DistTransitionCache,DistTransitionCache)).
81		synthesis_log_aux(distinguishing_transition_cache_changed(DistTransitionCache,NewDistTransitionCache)) :-
82		DistTransitionCache \= NewDistTransitionCache ,
83		format("~nCache has changed:~n",[]) ,
84		print_bexpr(DistTransitionCache) , nl.
85
86		synthesis_log_aux(expand_library) :-
87		format("~nExpand library.~n",[]).
88
89		synthesis_log_aux(two_non_equivalent_solutions(Type,Solution,FurtherSolution)) :-
90		format("~nFound two non equivalent ~w~nSolution: ~w~nFurther solution: ~w~n",[Type,Solution,FurtherSolution]).
91
92		synthesis_log_aux(distinguishing_error(error,ProgramAST,ProgramAST2)) :-
93		format("~nError when searching for a distinguishing input for programs ~w~n~w~n~n",[ProgramAST,ProgramAST2]).
94		synthesis_log_aux(distinguishing_error(_,_,_)).
95
96		synthesis_log_aux(start_synthesis_loop(DistTransitionCache,DistStateCache,Library,LibExpansion,CurrentVars,PreCondVars,
97		ValidInvariantsOrGuards,Type,PosInput,NegInput,LocationVars,M1,ParameterAmount,Solution)) :-
98		format("~nEnter synthesis loop for type ~w.~n",[Type]) ,
99		format("Distinguishing transition cache: ~w~nDistinguishing state cache: ~w~nLibrary: ~w~nLibrary expansion: ~w~n",
100		[DistTransitionCache,DistStateCache,Library,LibExpansion]) ,
101		format("Current variables: ~w~nVariables affected in simultaneous guard (only for operations): ~w~n",[CurrentVars,PreCondVars]) ,
102		(Type = action
103		-> format("Valid invariants or guards: ~w~nInput: ~w~nOutput: ~w~nLocation variables: ",[ValidInvariantsOrGuards,PosInput,NegInput])
104		; format("Valid invariants or guards: ~w~nPositive: ~w~nNegative: ~w~nLocation variables: ",[ValidInvariantsOrGuards,PosInput,NegInput])) ,
105		print_location_variables(LocationVars) ,
106		pp_io(PosInput,NegInput) ,
107		format("Line amount (M1): ~w~nParameter amount: ~w~nSolution: ~w~n",[M1,ParameterAmount,Solution]).
108
109		synthesis_log_aux(location_vars_to_program_and_fail(Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Solution)) :-
110		format("~nERROR: location_vars_to_program/9 failed, probably a wrong library configuration or the line amount does not fit the library size.~n",[]) ,
111		format("Type: ~w~nLibrary: ~w~nLocationVarsIn: ~w~nLocationVarsOut: ~w~nParameter: ~w~n,Solution: ~w~n.",
112		[Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Solution]) , !.
113
114		% this should be fixed and will hopefully never happen again, just to make sure
115		synthesis_log_aux(defective_further_solution_and_fail(Type,NewBehavioralConstraint,FurtherSolution,PosInput,NegInput,LocationVars,ProgramAST)) :-
116		Type \= action ,
117		FurtherSolution = solution(_) ,
118		ProgramAST = b(_,integer,_) , ! ,
119		format("~nError found in further solution.~n",[]) ,
120		format("Positive States: ~w~nNegative States: ~w~nFurther solution: ~w~nLocation variables: ~w~nBehavioral constraint:",
121		[PosInput,NegInput,FurtherSolution,LocationVars]) ,
122		print_bexpr(NewBehavioralConstraint) , nl , !.
123		synthesis_log_aux(defective_further_solution_and_fail(_,_,_,_,_,_,_)).
124
125		synthesis_log_aux(solve_distinguishing_constraint(DistConstraint,Solver)) :-
126		format("Try to find a distinguishing example:~nSolver: ~w~nDistinguishing constraint:~n",[Solver]) ,
127		translate:print_bexpr(DistConstraint) , nl ,
128		print(DistConstraint) , nl , nl.
129
130		pp_io(PosInput,NegInput) :-
131		format("Positive Examples:~n",[]) ,
132		pp_io_aux(0,PosInput) ,
133		format("Negative Examples:~n",[]) ,
134		pp_io_aux(0,NegInput).
135
136		pp_io_aux(_,[]).
137		pp_io_aux(C,[Example|T]) :-
138		format("Example #~w:~n",[C]) ,
139		pp_state(Example) ,
140		C1 is C + 1 ,
141		pp_io_aux(C1,T).
142
143		pp_state([]).
144		pp_state([IdValueAst|T]) :-
145		IdValueAst = b(_,_,Info) ,
146		member(synthesis(machinevar,VarName),Info) ,
147		format(" ~w:",[VarName]) ,
148		print_bexpr(IdValueAst) , nl ,
149		pp_state(T).
150
151		print_location_variables([]).
152		print_location_variables([LocationVar|T]) :-
153		print(LocationVar) , nl ,
154		print_location_variables(T).