Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / readme-simulation.txt @ 22fe1c93

History | View | Annotate | Download (1.04 KB)

1
Sources for benchmarks:
2

    
3

    
4
cd*, Gas*: based on problems by Bertrand Jeannet (courtesy Anders Franzen)
5

    
6
hysteresis*, speed*: Based on problems from 
7
  N. Halbwachs, P Raymond "A Tutorial of Lustre", 2002
8

    
9
car*, metros*, PRODUCER_CONSUMER*: based on problems by David Merchant* 
10
  (courtesy Anders Franzen)
11

    
12
production_cell*: based on problems from
13
  Leszek Holenderski. "Production Cell in {Lustre} -- A Case Study."
14
  Formal Development of Reactive Systems: Case Study Production Cell.
15
  Claus Lewerentz and Thomas Lindner, ed.  Springer-Verlag, 1995.  pp 104-112.
16

    
17
tramway*: based on problems from  
18
  Matthieu Moy, implementing an idea from Pascal Raymond
19

    
20
fast*, ums*: based on problems from
21
  Magnus Ljung. Formal modelling and automatic verification of lustre programs
22
  using NP-Tools. Master's thesis, Royal Institute of Technology,
23
  1999.  (Courtesy of Anders Franzen)
24

    
25

    
26
Please note that many of these benchmarks contain deliberately introduced
27
modifications to alter their behaviors, and do not necessarily reflect the
28
original creator's design intentions.