(************************************************************ * IMITATOR MODEL * * SIMOP * * Description : Networked automation system * Correctness : TODO * Source : SIMOP Project / Étienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg and Silvain Ruel. Synthèse de contraintes temporisées pour une architecture d’automatisation en réseau. In Didier Lime and Olivier H. Roux (eds.), MSR’09, Journal Européen des Systèmes Automatisés 43(7-9), Hermès, pages 1049–1064, 2009. * Author : Étienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg and Silvain Ruel * Modeling : ?, Étienne André, Laurent Fribourg * Input by : ?, Étienne André, Laurent Fribourg * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : 2020/08/19 * Last modified : 2020/08/19 * * IMITATOR version: 3 ************************************************************) (************************************************************) (* Property specification *) (************************************************************) property := #synth EF(loc[ENV] = ENV5);