synthesis_log_aux(solution_tuple(ProgramAST1,ProgramAST2)) :-
format("~nFound two eventually equivalent solutions:~n~w~n",[ProgramAST1]) ,
nl , print_bexpr_or_subst(ProgramAST1) , nl ,
print_bexpr_or_subst(ProgramAST2) , nl.
synthesis_log_aux(solution(_,none)) :-
format("~nSynthesis failed.~n",[]).
synthesis_log_aux(solution(_,state(State))) :-
format("~nDistinguishing State: ~w~n",[State]).
synthesis_log_aux(solution(_,transition(InputState,OutputState))) :-
format("~nDistinguishing Transition: ~w --> ~w~n",[InputState,OutputState]).
synthesis_log_aux(solution(Type,Solution)) :-
synthesis_log_aux(solution_enter(Type)) ,
synthesis_log_aux(solution_aux1(Type,Solution)).
synthesis_log_aux(solution_aux1(action,Action)) :-
\+is_list(Action) , ! ,
synthesis_log_aux(solution_aux2(action,[Action])).
synthesis_log_aux(solution_aux1(action,Actions)) :-
synthesis_log_aux(solution_aux2(action,Actions)).
synthesis_log_aux(solution_aux1(Type,Solution)) :-
Type \= action ,
print_bexpr_or_subst(Solution) , nl.
synthesis_log_aux(solution_aux2(action,[])).
synthesis_log_aux(solution_aux2(action,[Action|T])) :-
print_bexpr_or_subst(Action) , nl ,
synthesis_log_aux(solution_aux2(action,T)).
synthesis_log_aux(solution_enter(Type)) :-
(Type = action -> PrintType = operation ; PrintType = Type) ,
format("~nSynthesized ~w:~n",[PrintType]).
synthesis_log_aux(symmetry_reduction(SymmetryReduction)) :-
format("~nSymmetry reduction:~n",[]) ,
print_bexpr(SymmetryReduction) , nl.
synthesis_log_aux(relax_guard(OpName)) :-
format("~nStart synthesizing relaxed guard for operation ~w ~n",[OpName]).
synthesis_log_aux(invariant_violation_initialisation_state(Init)) :-
format("~nInvariant violation in initialisation state ~w",[Init]).
synthesis_log_aux(invariant_violation_found(State,Operation)) :-
format("~nInvariant violation in state ~w, caused by operation ~w ~n",[State,Operation]).
synthesis_log_aux(involved_variables(VarNames)) :-
format("~nVariables involved in invariant violation: ~w.~n",[VarNames]).
synthesis_log_aux(synthesize_new_guard_if_loop) :-
format("~nSynthesize new precondition for an operation that fits the current example.~n",[]).
synthesis_log_aux(distinguishing_constraint(Type,Constraint)) :-
format("~nDistinguishing constraint for type ~w:~n",[Type]) ,
print_bexpr(Constraint) , nl.
synthesis_log_aux(distinguishing_transition_cache_changed(DistTransitionCache,DistTransitionCache)).
synthesis_log_aux(distinguishing_transition_cache_changed(DistTransitionCache,NewDistTransitionCache)) :-
DistTransitionCache \= NewDistTransitionCache ,
format("~nCache has changed:~n",[]) ,
print_bexpr(DistTransitionCache) , nl.
synthesis_log_aux(expand_library) :-
format("~nExpand library.~n",[]).
synthesis_log_aux(two_non_equivalent_solutions(Type,Solution,FurtherSolution)) :-
format("~nFound two non equivalent ~w~nSolution: ~w~nFurther solution: ~w~n",[Type,Solution,FurtherSolution]).
synthesis_log_aux(distinguishing_error(error,ProgramAST,ProgramAST2)) :-
format("~nError when searching for a distinguishing input for programs ~w~n~w~n~n",[ProgramAST,ProgramAST2]).
synthesis_log_aux(distinguishing_error(_,_,_)).
synthesis_log_aux(start_synthesis_loop(DistTransitionCache,DistStateCache,Library,LibExpansion,CurrentVars,PreCondVars,
ValidInvariantsOrGuards,Type,PosInput,NegInput,LocationVars,M1,ParameterAmount,Solution)) :-
format("~nEnter synthesis loop for type ~w.~n",[Type]) ,
format("Distinguishing transition cache: ~w~nDistinguishing state cache: ~w~nLibrary: ~w~nLibrary expansion: ~w~n",
[DistTransitionCache,DistStateCache,Library,LibExpansion]) ,
format("Current variables: ~w~nVariables affected in simultaneous guard (only for operations): ~w~n",[CurrentVars,PreCondVars]) ,
(Type = action
-> format("Valid invariants or guards: ~w~nInput: ~w~nOutput: ~w~nLocation variables: ",[ValidInvariantsOrGuards,PosInput,NegInput])
; format("Valid invariants or guards: ~w~nPositive: ~w~nNegative: ~w~nLocation variables: ",[ValidInvariantsOrGuards,PosInput,NegInput])) ,
print_location_variables(LocationVars) ,
pp_io(PosInput,NegInput) ,
format("Line amount (M1): ~w~nParameter amount: ~w~nSolution: ~w~n",[M1,ParameterAmount,Solution]).
synthesis_log_aux(location_vars_to_program_and_fail(Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Solution)) :-
format("~nERROR: location_vars_to_program/9 failed, probably a wrong library configuration or the line amount does not fit the library size.~n",[]) ,
format("Type: ~w~nLibrary: ~w~nLocationVarsIn: ~w~nLocationVarsOut: ~w~nParameter: ~w~n,Solution: ~w~n.",
[Type,Library,LocationVarsIn,LocationVarsOut,Parameter,Solution]) , !.
synthesis_log_aux(defective_further_solution_and_fail(Type,NewBehavioralConstraint,FurtherSolution,PosInput,NegInput,LocationVars,ProgramAST)) :-
Type \= action ,
FurtherSolution = solution(_) ,
ProgramAST = b(_,integer,_) , ! ,
format("~nError found in further solution.~n",[]) ,
format("Positive States: ~w~nNegative States: ~w~nFurther solution: ~w~nLocation variables: ~w~nBehavioral constraint:",
[PosInput,NegInput,FurtherSolution,LocationVars]) ,
print_bexpr(NewBehavioralConstraint) , nl , !.
synthesis_log_aux(defective_further_solution_and_fail(_,_,_,_,_,_,_)).
synthesis_log_aux(solve_distinguishing_constraint(DistConstraint,Solver)) :-
format("Try to find a distinguishing example:~nSolver: ~w~nDistinguishing constraint:~n",[Solver]) ,
translate:print_bexpr(DistConstraint) , nl ,
print(DistConstraint) , nl , nl.