[ file[.svl] [script-parameters]]
svl -script options [ file1[.svl] ] [ -output file2 ]
svl -expand [-case] [-indent n] [ file1[.svl] ] [ -output file2 ]
svl -clean [ file[.svl] ]
svl -sweep [ file[.svl] ]
where the following options are available:
-case, -debug, -ignore, -sh sh-options, -silent.
In the simplest form (first line of the synopsis), taking as input file.svl, which contains a verification script in SVL (Script Verification Language), svl produces actions invoking CADP tools. See svl-lang for a description of the SVL language.
svl runs a given script through the following steps:
During script execution, several temporary intermediate files may be created, and removed as soon as possible in order to minimize disk space consumption. svl also maintains a log file named file.log that contains a full diagnostic of the script execution.
Note that file.svl (or file1.svl) can be omitted if there exists a unique file with extension .svl in the current directory, in which case this file is considered as the input.
svl_kernelwill be searched in $SVL/bin.`arch` instead of $CADP/bin.`arch`.
svl version 2.0 and later: Hubert Garavel, Frederic Lang, Marc Herbert.
svl versions 1.0 to 1.6 (kept for internal use and never distributed officially): Mark Jorgensen, Christophe Discours, Hubert Garavel.
The authors owe thanks to Radu Mateescu and Charles Pecheur for their feedback about svl 1.* and to Laurent Mounier for his useful advices.
+--------------+-------------------------+-----+-----+-----+ | Extension | Description | In | Out | Tmp | +--------------+-------------------------+-----+-----+-----+ | .lnt | LNT program | X | | | | .lotos .lot | LOTOS program | X | | | | .lts | FSP program | X | | | | .aut | LTS in Aldebaran format | X | X | X | | .bcg | LTS in BCG format | X | X | X | | .fc2 | LTS in FC2 format | X | X | X | | .seq | LTS in sequence format | X | X | | | .exp | network of LTSs | X | X | X | | .hide .hid | labels to hide | X | | X | | .cut | labels to cut | X | | X | | .rename .ren | labels to rename | X | | X | | .sync | labels to synchronize | X | | X | | .mcl | temporal logic formula | X | | | | .log | log of execution | | X | | +--------------+-------------------------+-----+-----+-----+Note: svl generates temporary files in the current directory. To avoid clashes with existing files, file names generated by svl are prefixed with a string of the form
_, where xxx is a 3 digits number. Hence it is recommended to avoid naming user files this way.
[GL01] Hubert Garavel and Frederic Lang. SVL: a Scripting Language for Compositional Verification. In Myungchul Kim, Byoungmoon Chin, Sungwon Kang, and Danhyung Lee (editors), Proceedings of the 21st International Conference on Formal Techniques for Networked and Distributed Systems FORTE'2001 (Cheju Island, Korea), IFIP Conference Proceedings volume 197, pages 377-394, Kluwer, August 2001. Available from http://cadp.inria.fr/publications/Garavel-Lang-01.html
[GLM15] Hubert Garavel, Frederic Lang, and Radu Mateescu. Compositional Verification of Asynchronous Concurrent Systems using CADP. Acta Informatica, Special Issue on Combining Compositionality and Concurrency: Part 2, 52(4-5):337-392, 2015. Available from http://cadp.inria.fr/publications/Garavel-Lang-Mateescu-15.html
[KM97] Jean-Pierre Krimm and Laurent Mounier. Compositional State Space Generation from LOTOS Programs. In Ed Brinksma (editor), Proceedings of TACAS'97 Tools and Algorithms for the Construction and Analysis of Systems (University of Twente, Enschede, The Netherlands), Lecture Notes in Computer Science volume 1217, Springer, April 1997. Available from http://cadp.inria.fr/publications/Krimm-Mounier-97.html
[Lan02] Frederic Lang. Compositional Verification using SVL Scripts. In Joost-Pieter Katoen and Perdita Stevens (editors), Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems TACAS'2002 (Grenoble, France), Lecture Notes in Computer Science volume 2280, pages 465-469, Springer, April 2002. Available from http://cadp.inria.fr/publications/Lang-02.htmlaldebaran , bcg_cmp , bcg_graph , bcg_io , bcg_labels , bcg_min , bcg_open , caesar , caesar.adt , caesar.open , caesar_hide_1 , caesar_rename_1 , evaluator , exhibitor , exp.open , generator , projector , reductor , regexp , seq.open , svl-lang
Directives for installation are given in files $CADP/INSTALLATION_*.
Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.firstname.lastname@example.org