InSPEQTor

This tool (standing for INference of Shortest Paths with EQuivalent Time-abstract behaviOR) is an implementation of the inverse method in the framework of Parametric Directed Weighted Graphs.

InSPEQTor takes as an input a Parametric Directed Weighted Graph, and a reference valuation for each parameter. It can synthesize two constraints on the weights of the graph seen as parameters:

In the first case, each shortest path in the graph instantiated with the reference valuation is also a shortest path for any parameter valuation satisfying the constraint (and conversely).

In the second case (coming from the Max−Plus Algebra), each circuit of maximal mean in the graph instantiated with the reference valuation is also a circuit of maximal mean for any parameter valuation satisfying the constraint (and conversely).

InSPEQTor has been developed in OCaml by Étienne André in 2009-2010 at Laboratoire Spécification et Vérification, ENS Cachan, France. It is provided under the GNU-GPL license.

Using InSPEQTor

InSPEQTor takes as input a text file describing a Parametric Directed Weighted Graph, including the reference value for each parameter.

The syntax is described in a functional style, with OCaml-style (possibly nested) comments.

The call syntax is:

./INSPEQTOR [file.ins]

The result is given directly in the terminal.

By default, InSPEQTor synthesize constraints guaranteeing the preservation of shortest paths. To run InSPEQTor in order to synthesize constraints guaranteeing the preservation of circuits of maximal mean, use option -maxplus.

Download and Install

Version Release Source (tar.bz2) Source (zip) Binary
0.2 13th September 2010 InSPEQTor.tar.bz2 (26Ko) InSPEQTor.zip (34Ko) INSPEQTOR (201Ko)
0.1 25th May 2009

The binary is a standalone binary for Ubuntu; it has been compiled using Ubuntu 10.10. If it doesn’t work, please compile the source code.

Examples

Name File
Toy example exemple.ins
Example from book "Initiation à l’algorithmique" p.551 exLivralgo.ins
Going from Place d’Italie to LSV PlacedItalieLSV.ins
Going from Rennes to LSV RennesLSV.ins
Going from Rennes to LSV (alternative version) RennesLSV2.ins
Going from Rennes to LSV (Ph.D. thesis manuscript version) RennesLSVthese.ins

Contact

References