```// ************************************************************************** //
//                                                                            //
//    eses                   eses                                             //
//   eses                     eses                                            //
//  eses    eseses  esesese    eses   Embedded Systems Group                  //
//  ese    ese  ese ese         ese                                           //
//  ese    eseseses eseseses    ese   Department of Computer Science          //
//  eses   eses          ese   eses                                           //
//   eses   eseses  eseseses  eses    University of Kaiserslautern            //
//    eses                   eses                                             //
//                                                                            //
// ************************************************************************** //
// The module below describes a RS-Flipflop constructed with NOR-gates        //
// that have the same delay. This delay is modeled as a macro step of         //
// Quartz. We then prove some facts about the stability of the circuits.      //
// ************************************************************************** //

macro InputChange = ((s<->!X s) | (r<->!X r));

module RSFlipFlop(bool ?r,?s,p,q){
loop {
next(p) = !(s | q);
next(q) = !(r | p);
pause;
}
} satisfies {
// ------------------------------------------------------
// The following specs state that once a certain input
// is given, then a stable output is obtained after some
// delay time. To allow arbitrary delays, we have to fix
// the input forever.
// ------------------------------------------------------
Set :       assert A G ( G( s & !r) -> F G (!p &  q) );
Reset :     assert A G ( G(!s &  r) -> F G ( p & !q) );
Forbidden : assert A G ( G( s &  r) -> F G (!p & !q) );
// ------------------------------------------------------
// The spec below states that the outputs oscillate when
// the inputs s and r are both false at a point of time
// where the outputs p and q are different.
// ------------------------------------------------------
Oscillate : assert A G ( G (!s & !r & (p <-> q))
-> G ((X p <-> !p) & (X q <-> !q)) );
// ------------------------------------------------------
// The spec below states that the outputs oscillate when
// the inputs s and r are both false at a point of time
// where the outputs p and q are different.
// ------------------------------------------------------
NoOscilla : assert A G ( G (!s & !r & (p <-> !q))
-> G ((X p <-> p) & (X q <-> q)) );
// ------------------------------------------------------
// We conclude that all inputs are stable when p is not
// equal to q. This is proved below
// ------------------------------------------------------
StableOutputs1:
assert A (  G(p <->  !q) &
G(s <-> X s) &
G(r <-> X r) ->
F G ( (p <-> X p) & (q <-> X q)));
// ------------------------------------------------------
// This suggests the following operation mode: we assume
// that at some point of time, we have (r <-> !s). This
// either sets or resets the flipflop, and in particular,
// we then have p!=q. If after that point of time, the
// input s=r=1 never occurs, then we always have stable
// outputs. However, the property StableOutputs2 below
// is not true.
// ------------------------------------------------------
//    StableOutputs2:
//  assert A G ((s <-> !r) &
//           G!(s & r) &
//           F G ((s <-> X s) & (r <-> X r))
//           ->
//           F G ((p <-> X p) & (q <-> X q)));
// ------------------------------------------------------
// The problem that appears with the above specification
// is that the inputs change too fast. An stable input
// like s&!r can lead to transient transitions. For example,
// !r&s&p&!q -> X(!p&!q), and when the same input would
// still be available, we would reach output !p&q next.
// ------------------------------------------------------
StableOutputsWithSlowInputs:
assert A (  F(s <-> !r) &
G (InputChange -> X !InputChange) &
G !(s & r) &
F G ((s <-> X s) & (r <-> X r))
->
F G ((p <-> X p) & (q <-> X q)));
// ------------------------------------------------------
// Finally, we list all transitions, which explains the
// delay time we used above: There are transitient moves
// of length 2.
// ------------------------------------------------------
AllTransitions:
assert A G ((!r & !s & !p & !q -> X( p &  q)) &
(!r & !s & !p &  q -> X(!p &  q)) &
(!r & !s &  p & !q -> X( p & !q)) &
(!r & !s &  p &  q -> X(!p & !q)) &
(!r &  s & !p & !q -> X(!p &  q)) &
(!r &  s & !p &  q -> X(!p &  q)) &
(!r &  s &  p & !q -> X(!p & !q)) &
(!r &  s &  p &  q -> X(!p & !q)) &
( r & !s & !p & !q -> X( p & !q)) &
( r & !s & !p &  q -> X(!p & !q)) &
( r & !s &  p & !q -> X( p & !q)) &
( r & !s &  p &  q -> X(!p & !q)) &
( r &  s & !p & !q -> X(!p & !q)) &
( r &  s & !p &  q -> X(!p & !q)) &
( r &  s &  p & !q -> X(!p & !q)) &
( r &  s &  p &  q -> X(!p & !q)));
}
```