PROSPER AT EDINBURGH

Proof and Specification Assisted Design Environments

Convert a sentence to CTL


Either select an example:

If sig2 is high then sig3 is low.
If sig1 is active then if sig2 is high then sig3 is low.
If sig1 is active if sig2 is high then sig3 is low.
Sig1 is high until the point when sig2 is low.
Sig1 is high until sig2 is low.
Two cycles after sig1 is active, sig2 is active.
Sig1 is high for 3 cycles.
Sig1 and sig2 are different.
After sig1 is high sig2 is low until the point when sig3 is high.

...or type in your own sentence:


Which representations?

CTL only
Most representations (no textnorm or sem)
All representations

This system makes use of the Alvey Natural Language Tools.

25 November 1999