(************************************************************ * IMITATOR MODEL * * Jobshop case study * * Description : Jobshop case study * Correctness : All tasks performed on time * Source : Maler et al. ("Job-Shop Scheduling Using Timed Automata", by Yasmina Abdeddaïm and Oded Maler, CAV 2001 (??)) Source of this parameter valuation: unknown * bibkey : AM01 * Author : Romain Soulat * Modeling : Romain Soulat * Input by : Romain Soulat, Étienne André * License : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0) * * Created : ? * Last modified : 2020/08/17 * * IMITATOR version: 3.0 ************************************************************) property := #synth IM( d11 = 3 & d12=6 & d13=1 & d14=7 & d21=10 & d22=8 & d23=5 & d24=4 );