Model checker analysing B & O example. Added one more rule in the formula embedding to deal with tock transitions in the sequential composition construct.