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.
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.
| 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.
| 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 |