-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES) -- http://cadp.inria.fr [Last updated: Thu Oct 6 11:18:41 CEST 2022] This directory contains an example for LNT2LOTOS, CAESAR, CAESAR.ADT, BISIMULATOR, OPEN/CAESAR, and TGV. It describes the INRES (Initiator Responder) protocol, which is a simplified version of the ABRACADABRA protocol. The original version of INRES protocol and service are described in: Dieter Hogrefe OSI Formal Specification Case Study: the INRES protocol and service Institut Fur Informatik, Universitat Bern, April 1991 The original version has been corrected and improved by Ana Cavalli's team at Institut National des Telecommunications (INT, Evry, France). Various reports have been written, for instance: Hok Hiong Pang Generation of a Finite State Machine From a LOTOS Specification of INRES Protocol using CAESAR Institut National des Telecommunications, Evry, France This directory provides various versions in LOTOS of the INRES protocol and service, by courtesy of INT. The LOTOS specifications have been translated to LNT by Hubert Garavel, on the basis of a student project done by Almer Bolatov (Saarland University, Germany). Files: LOTOS/inres_service_original.lotos original specification of the service by D. Hogrefe LOTOS/inres_service_japan.lotos improved version of the service provided by Japanese researchers LOTOS/inres_service_int.lotos service specification by K. H. Pang (INT) - this is the version we use LOTOS/INRES_SERVICE.lib data type library for the service inres_service_int.lnt service specification written in LNT LOTOS/inres_protocol_original.lotos original specification of the protocol by D. Hogrefe LOTOS/inres_protocol_int_4.lotos version 4 of the protocol by P. Maigron (INT): with deadlocks LOTOS/inres_protocol_int_5.lotos version 5 of the protocol by K. H. Pang (INT): debugged specification, no coder LOTOS/inres_protocol_int_6.lotos version 6 of the protocol, by K. H. Pang (INT): debugged specification, no coder, lossy channel - this is the version we use LOTOS/INRES_PROTOCOL.lib data type library for the protocol inres_protocol_int_6.lnt protocol specification written in LNT inres_service_tp.aut test purpose for the TGV tool inres_service_int.io input/output actions for the TGV tool sequence_*.seq Message Sequence Charts describing allowed execution sequences of the INRES protocol Note: currently, the maximal number of ISDU sent by the Initiator is fixed to 1. This can be changed by adding new constructors (data2, data3, ...) to sort ISDU (type ISDUType in file INRES_PROTOCOL.lib) The file "demo.svl" describes the verification of the service and protocol. You can execute it by typing: $ svl demo or even simply $ 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 interactively a description of the protocol, e.g., using XSIMULATOR: $ lnt.open inres_protocol_int_6.lnt xsimulator