CirView: Visualization of LTL Path Checking Via Boolean Circuits

[2010-02-26, version 0.4, rev. c7f4e9d83ba7]

Coypright © 2010 Saarland Univerisity

Introduction

CirView is a small tool for visualizing the construction and evaluation of boolean circuits that represent the value of a formula in linear time temporal logic (LTL) over a finite trace. A trace is an interpretation of the propositions of the formula over the course of time. The circuits are visualized and animated in 3D. The tool demonstrates the evaluation of a circuit using the parallel contraction algorithm described in [KF09]. It is part of a larger library for investigating different evaluation strategies and their implementation for boolean circuits for LTL path checking. We will support the visualization of a broader range of evaluation strategies from that library in the upcoming releases of the tool.

Publications

Usage

For usage information call the tool as CirView --help.

The circuits are visualized via GLUT/openGL. We think the animation is reasonably smooth. However, we have not optimized the rendering code. Make sure you have hardware accelerated graphics and better not run the binary remotely.

Documentation

The tool itself is quite verbose about its usage. If you have questions please contact Lars Kuhtz.

Download

You can download and use CirView under the terms of the following LICENSE.

Current version

0.4 [2010-03-05, rev. c7f4e9d83ba7, linux x86-64bit]

Contact

Lars Kuhtz <kuhtzXcsYuni-sbYde> (substitute X by @ and Y by .)