TeamAmalgam / kodkod

Kodkod relational model finder
Other
3 stars 0 forks source link

Use StringBuilder to combine multiline logging #22

Closed mhyee closed 11 years ago

mhyee commented 11 years ago

Using logger.log() for every single line of multi-line output makes the output really messy.

I changed it to use a StringBuilder to build up the message, and then I output it once.

This changes the logging from

FINE: Found a solution. At time: 3, Improving on [76, 85]
Jul 05, 2013 9:18:17 AM kodkod.multiobjective.MetricPoint parametrizedImprovementConstraints
FINE: Possible Improvements are conjunction of
Jul 05, 2013 9:18:17 AM kodkod.multiobjective.MetricPoint parametrizedImprovementConstraints
FINE:   (sum((this/ConcreteKnapsack . this/Knapsack.metric0)) >= 76)
Jul 05, 2013 9:18:17 AM kodkod.multiobjective.MetricPoint parametrizedImprovementConstraints
FINE:   (sum((this/ConcreteKnapsack . this/Knapsack.metric1)) >= 85)
Jul 05, 2013 9:18:17 AM kodkod.multiobjective.MetricPoint parametrizedImprovementConstraints
FINE:   ((sum((this/ConcreteKnapsack . this/Knapsack.metric0)) > 76) || (sum((this/ConcreteKnapsack . this/Knapsack.metric1)) > 85))
Jul 05, 2013 9:18:17 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm multiObjectiveSolve
FINE: Found Pareto point with values: [76, 85]
Jul 05, 2013 9:18:19 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm multiObjectiveSolve
FINE: Magnifying glass found 1 solution(s). At time: 5
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: # Sat Call: 14
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: # Unsat Call:  2
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Total Time in Sat Calls: 2,806
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Total Time in Sat Calls Solving: 524
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Total Time in Sat Calls Translating: 2,282
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Total Time in Unsat Calls: 1,747
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Total Time in Unsat Calls Solving: 472
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Total Time in Unsat Calls Translating: 1,275
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: # Magnifier Sat Call: 1
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: # Magnifier Unsat Call: 1
Jul 05, 2013 9:18:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Total Time in Magnifier: 1,843

to

Jul 05, 2013 9:19:19 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm multiObjectiveSolve
FINE: Found a solution. At time: 2, Improving on [76, 85]
Jul 05, 2013 9:19:19 AM kodkod.multiobjective.MetricPoint parametrizedImprovementConstraints
FINE: Possible Improvements are conjunction of
    (sum((this/ConcreteKnapsack . this/Knapsack.metric0)) >= 76)
    (sum((this/ConcreteKnapsack . this/Knapsack.metric1)) >= 85)
    ((sum((this/ConcreteKnapsack . this/Knapsack.metric0)) > 76) || (sum((this/ConcreteKnapsack . this/Knapsack.metric1)) > 85))
Jul 05, 2013 9:19:19 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm multiObjectiveSolve
FINE: Found Pareto point with values: [76, 85]
Jul 05, 2013 9:19:21 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm multiObjectiveSolve
FINE: Magnifying glass found 1 solution(s). At time: 4
Jul 05, 2013 9:19:23 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm multiObjectiveSolve
FINE: All Pareto points found. At time: 6
Jul 05, 2013 9:19:23 AM kodkod.multiobjective.algorithms.IncrementalGuidedImprovementAlgorithm debugWriteStatistics
FINE: Solver statistics:
    # Sat Call: 14
    # Unsat Call: 2
    # Total Time in Sat Calls: 2598
    # Total Time in Sat Calls Solving: 469
    # Total Time in Sat Calls Translating: 2129
    # Total Time in Unsat Calls: 1732
    # Total Time in Unsat Calls Solving: 447
    # Total Time in Unsat Calls Translating: 1285
    # Magnifier Sat Call: 1
    # Magnifier Unsat Call: 1
    # Total Time in Magnifier: 1817

I also added the logging line: All Pareto points found. At time: x

Reviewers: @AtulanZaman @cpkleynhans @joseph2625

joseph39 commented 11 years ago

Looks good.

cpkleynhans commented 11 years ago

LGTM

mhyee commented 11 years ago

In hindsight, this makes it more difficult to use grep to filter out certain logging levels. (And grep can already be used in the previous version to filter out the extraneous logging messages.)

However, I think that's a small cost to gain significantly more readable output.