🚀 go-pugleaf

In article <1992Oct15.211956.22851@wuecl.wustl.edu> wilcox@swarm.wustl.edu
 (Don Wilcox) writes:

> Almost every paper in formal methods, software engineering, or system
> specification uses examples, and most of the papers describing new ideas use
> fairly simple examples. ...  would you be interested in telling
> me about your favorite "toy" example? 

A new one I saw recently was "Cat and Mouse": a mouse runs past a cat, 
after a delay the cat begins pursuing the mouse.  Can the cat capture the 
mouse before the mouse escapes through a hole in the wall?  This was posed
to participants in a workshop on real time systems.

This very long paper proposes a Statechart solution (and discusses several
other problems and notations also):

@inproceedings{author = "Oded Mahler and Zohar Manna and Amir Pnueli",
	title = "From Timed to Hybrid Systems",
	pages = "445 -- 484",
	booktitle = "Real-Time: Theory in Practice,
			{REX} Workshop Proceedings",
	year=1991,
	editor="J. W. de Bakker and C. Huizing and W. P. de Roever and 
			G. Rozenberg",
	publisher="Springer-Verlag",
	note="Lecture Notes in Computer Science 600"}

This short paper proposes a Z solution:

@inproceedings{author = "William G. Wood",
	title = "A Specification of the Cat and Mouse Problem",
	pages = 676 -- 686,

	... other information as in preceding reference ...

	}

- Jon Jacky, jon@radonc.washington.edu, University of Washington, Seattle USA