Sources for benchmarks: cd*, Gas*: based on problems by Bertrand Jeannet (courtesy Anders Franzen) hysteresis*, speed*: Based on problems from N. Halbwachs, P Raymond "A Tutorial of Lustre", 2002 car*, metros*, PRODUCER_CONSUMER*: based on problems by David Merchant* (courtesy Anders Franzen) production_cell*: based on problems from Leszek Holenderski. "Production Cell in {Lustre} -- A Case Study." Formal Development of Reactive Systems: Case Study Production Cell. Claus Lewerentz and Thomas Lindner, ed. Springer-Verlag, 1995. pp 104-112. tramway*: based on problems from Matthieu Moy, implementing an idea from Pascal Raymond fast*, ums*: based on problems from Magnus Ljung. Formal modelling and automatic verification of lustre programs using NP-Tools. Master's thesis, Royal Institute of Technology, 1999. (Courtesy of Anders Franzen) Please note that many of these benchmarks contain deliberately introduced modifications to alter their behaviors, and do not necessarily reflect the original creator's design intentions.