Tinker2 - TACAS 16 paper resources

Foreword

This webpage aims to present resources used for our tool presentation. To use those resources, first download Tinker from here. Once extracted, the example files will be available under:

$SOME_PATH/tinker/src/core/demo/TACAS16/

The example runs with Proof Power, to configure it, follow those steps :

• assume that the quantomatics repo and the psgraph are cloned in the same folder, for example

  $SOME_PATH/tinker

  we can check the readme file to make sure the path is correct, e.g. the readme for quantomatoics repo will be

  $SOME_PATH/tinker/quantomatic/README

  similarly, the readme for the psgtarph repo will be

  $SOME_PATH/tinker/psgraph/Readme.md?

  Note that both repo need to be latest version.

• go to the tinker folder by

  cd $SOME_PATH/tinker

  then to make the psgraph db, using

  pp_make_database -p zed psgraph

• then to open the psgraph db in the same directory, i.e.

  xpp -d psgraph

• in the xpp, to open the install file in

  $SOME_PATH/tinker/psgraph/src/core/provers/proofpower/build/install.ML

  then to run this run to compile the required library into the psgraph db.

• now the psgraph db should be ok to load psgraph and run and run some experiments, no need to do steps 1 - 4 from this point.

• to run some examples, open the psgraph db under

  $SOME_PATH/tinker

  by

  xpp -d psgraph

Then open the following demo file in the pp to see if the tool can run correctly

$SOME_PATH/tinker/psgraph/src/core/demo/TACAS16/

The line

PPIntf.set_psg_goal

is to ask pp to connect gui for proofs. Note that to enable gui to accept the connection from pp, the following need to be clicked , once the connection is ready the icon will become . Details on how to start the GUI can be found in Tinker's user guide.

Proof recording

Tool demo

• Basic Drag and Drawing Editing
• Supports for Hierarchy
• PSGraph Library
• Evaluation and Debugging
• Breakpoint