Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Albert Camilleri <ac@gslxsrv.rose.hp.com>
Message-Id: <9410122129.AA02235@gslxsrv.rose.hp.com>
Subject: Re: Single Pulser
To: info-hol@cs.uidaho.edu (info-hol)
Date: Wed, 12 Oct 94 14:29:10 PDT
Cc: bobo@hprpcd.rose.hp.com (Bob Odineal)
Mailer: Elm [revision: 70.85]


For what it's worth, one little trick I have found when using SMV, which helps
*enormously* with reducing the complexity of the CTL specs, is to define
additional macros into the FSM model, and then to use these directly in the CTL
formulae. This can potentially make things much clearer (especially with
problems much more complex than the single pulser ;-).

To illustrate, in my proposed SMV solution to the single pulser (which Kathi
Fisler posted earlier) the use of a variable to denote the "rising edge" of
the input is helpful because it doesn't have to be expressed in terms of
temporal "next" operators inside the CTL spec each time it is needed.
(Obviously, such use of macros helps sort out the wood from the trees in most
 specification languages.)

So, if
	risingEdge(t+1) = i(t+1) & ~i(t)	 (to be expressed as a FSM)

the first part of the spec says that once you get a rising edge on the
input, then the output will always eventually go high.

	AG (risingEdge -> (AF o))

The second part says that once an output happens then it will immediately go
low on the next cycle (a single pulse), and it will stay low at least until
the next rising edge on the input. (max one output per rising edge).

	AG (o -> (AX (A [!o U risingEdge])))

And finally, the third part of the spec says that if the output does not
happen at the same time as the rising edge on the input, then there will be no
other rising edge until the output happens. (max one rising edge per output).

	AG (risingEdge -> (!o -> (AX (A [!risingEdge U o]))))

So the first part of the spec denotes liveness, and the second and third
together denote a 1:1 correspondence between input and rising edge.

***Now caution is required here.***

The above spec attempts to capture the notion of "neighbourhood" within which
the output must go high. The neighbourhood (as presented in Steve Johnson's
lecture at TPCD) is defined as the interval between successive rising edges on
the input. This presumes a special kind of input: one which goes low again
after it goes high!

Thus, the implementation suggested in the paper of making the output go high
on the falling edge of the input:
	o(t+1) = ~i(t+1) /\ i(t)
does not satisfy the above specification for all inputs, eg. in the case that
the input stays high forever! In such (an undesired) behaviour, the notion of
neighbourhood we adopted becomes infinite, so we need to put a constraint on
the input to be well-behaved if the spec is to make any sense. This can be
regarded as an implementation issue, of course, as opposed to one of
specification (depending on how loose a spec one desires).

In SMV, one abstract way of constraining the behaviour of the input would be by
using FAIRNESS constraints, eg

	FAIRNESS  risingEdge

which would prune the state space to only those FSMs in which rising edges
happened frequently often (i.e. to disregard cases where the input stayed high
forever, or low forever).

An overall SMV verification, therefore, of the implementation of the single
pulser presented in Steve's paper could be:

---------------------------------------------------------------

MODULE	main

VAR	i : boolean;			-- non-deterministically 0 or 1.

VAR	pi : boolean;			-- previous value of i, ie. pi(t+1) = i
ASSIGN	next (pi) := i;

DEFINE	o := pi & !i;			-- implementation of single pulser.
					-- (equivalent to input falling edge!)

DEFINE	risingEdge := i & !pi;		-- input rising edge.

FAIRNESS risingEdge			-- constrain input to "rise and fall"

SPEC	AG (risingEdge -> (AF o))
SPEC	AG (o -> (AX (A [!o U risingEdge])))
SPEC	AG (risingEdge -> (!o -> (AX (A [!risingEdge U o]))))

----------------------------------------------------------------

The result is rather simple, but I must confess to have only thought about the
matter for no more than several minutes, so there could well be mistakes from
what was originally intended, and of course, there could well be other simpler
and more elegant solutions.

--Albert

PS  Without using the additional benefit of expressing parts of the specs as
    FSMs, I have often found that expressivity in CTL alone can be a problem.
    With a combination of FSM and CTL, however, things can get a lot easier.
    One common example is referring to things which must have happened in the
    past: e.g. if X is true, then Y must have been true some time ago.
    This sort of thing becomes very easy if you can use FSMs to maintain
    "memory" (or state), and then to use that directly in the CTL specs.

--
-----------------------------------------------------------------
|  Albert J Camilleri		|				|
|  Hewlett-Packard Company	|				|
|  Systems Technology Division	|  Tel  : +1 916 785 8488	|
|  Mailstop R5/EF		|  Fax  : +1 916 785 3096	|
|  8000 Foothills Boulevard	|  Email: ac@hprpcd.rose.hp.com	|
|  Roseville, CA 95747		|				|
|  USA				|				|
-----------------------------------------------------------------