-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES) -- http://cadp.inria.fr [Last updated: Thu Oct 6 11:18:07 CEST 2022] This directory contains an example for BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, LNT2LOTOS, OPEN/CAESAR, and SVL. It describes a car overtaking protocol written in LNT and LOTOS. This example originates from the Swedish Institute of Computer Science It is described in detail in: P. Ernberg, L. Fredlund, B. Jonsson: Specification and Validation of a Simple Overtaking Protocol using LOTOS. SICS Technical Report T90006, 1990 It was translated to LNT by Hubert Garavel, on the basis of a student project done by Almer Bolatov (Saarland University, Germany). Files: overtaking.lnt LNT specification demo.svl SVL verification script false_property.aut automaton specifying a property true_property.aut automaton specifying a property LOTOS/overtaking.lotos LOTOS specification LOTOS/demo.svl SVL script The file "demo.svl" describes the verification of the protocol. You can execute it by typing: $ svl demo or even simply $ svl Detailed explanations on the verification scenario are given in "demo.svl". After execution of the SVL scenario, all generated files can be removed by typing $ svl -clean demo or even simply $ svl -clean You can also simulate the overtaking protocol interactively, using the OCIS interactive simulator. This is done by using the front-end shell script for OPEN/CAESAR: $ lnt.open -english overtaking.lnt ocis