$inputData = "
  one sig S extends System [ ] {
    nbrOfsup == 1 and
    states == S1 + S2 + S3 + S4 + S5 + S6 and
    events == Alpha + Beta + Gamma and
    ctrlEvents == Beta and
    ctrlEventSets == 1**Beta and
    obsEvents == Alpha + Beta and
    obsEventSets == 1**Alpha + 1**Beta and
    ctrlEventsE == Beta and
    ctrlEventsD == none
  }

  one sig G extends Automaton [ ] {
    states == S1 + S2 + S3 + S4 + S5 + S6 and
    labels == Alpha + Beta + Gamma and
    initialState == S1 and
    finalStates == states and
    transition == S1**Alpha**S2 + S1**Gamma**S4 + S2**Beta**S3 +
                  S4**Alpha**S5
  }

  one sig H extends Automaton [ ] {
    states == S1 + S2 + S3 + S4 + S5 and
    labels == Alpha + Beta + Gamma and
    initialState == S1 and
    finalStates == states and
    transition == S1**Alpha**S2 + S1**Gamma**S4 + S2**Beta**S3 +
                  S4**Alpha**S5
  }

  assertion c__observability {
    observability(S, G, H)
  }

  check :c__observability, 15, Int => 6, Walk => 7,
         System=>(exactly 1), Automaton=>(exactly 2), Labels=>(exactly 3),
         StateSpace=>(exactly 6)
"