The (timed) clause involvement visualization

The visualizations were obtained from the following log files:

Log fileGenerated by
hwmcc07-aigbmc-bc57sensorsp2negModified AIGBMC
hwmcc07-aigbmc-eijkS1238Modified AIGBMC
example-inductive-n3Modified AIGBMC
hwmcc11-aigbmc-pdtvisgigamax2Modified AIGBMC
musfinder-barrel5MUS Finder
musfinder-barrel5-rotateMUS Finder


The data was plotted using the bash shell script plot.sh. The script requires the tools gawk, gnuplot, ps2pdf and pdfcrop to be installed.

FigureGenerated by commandOutput file name
Figure 3.3
./plot.sh hwmcc07-aigbmc-bc57sensorsp2neg notime 80 notitle problem 110
hwmcc07-aigbmc-bc57sensorsp2neg_id=80-viz.pdf
Figure 3.4
./plot.sh hwmcc07-aigbmc-bc57sensorsp2neg notime 104 notitle problem 110
hwmcc07-aigbmc-bc57sensorsp2neg_id=104-viz.pdf
Figure 3.5
./plot.sh hwmcc07-aigbmc-bc57sensorsp2neg notime 110 notitle problem 110
hwmcc07-aigbmc-bc57sensorsp2neg_id=110-viz.pdf
Figure 3.6 and 4.6
./plot.sh hwmcc07-aigbmc-eijkS1238 notime 50 notitle problem
hwmcc07-aigbmc-bc57sensorsp2neg_id=80-viz.pdf
Figure 3.7
./plot.sh hwmcc07-aigbmc-bc57sensorsp2neg time 104 notitle
hwmcc07-aigbmc-bc57sensorsp2neg_id=104-timedviz.pdf
Figure 4.7
./plot.sh example-inductive-n3 notime 30 notitle
example-inductive-n3_id=30-viz.pdf
Figure 4.9
./plot.sh hwmcc11-aigbmc-pdtvisgigamax2 notime 57 notitle
hwmcc11-aigbmc-pdtvisgigamax2_id=57-viz.pdf
Figure 4.10
./plot.sh hwmcc11-aigbmc-pdtvisgigamax2 notime 58 notitle
hwmcc11-aigbmc-pdtvisgigamax2_id=58-viz.pdf
Figure 5.4
./plot.sh musfinder-barrel5 time 0 notitle noproblem
musfinder-barrel5_id=0-timedviz.pdf
Figure 5.5
./plot.sh musfinder-barrel5-rotate time 0 notitle noproblem
musfinder-barrel5-rotate_id=0-timedviz.pdf

See also the clause involvement visualization videos.