Issue found! Reporting path 0. Trace:
SpecificationStates Input -> ObservedOutput
    1: [S0] Button -> []
    2: [S0] Coin -> []
    3: [S1] Button -> [Tea]
    4: [S0] Coin -> []
    5: [S1] Button -> [Tea]
    6: [S0] Coin -> []
    7: [S1] Coin -> []
    8: [S2] Coin -> []
    9: [S2] Button -> []

Allowed outputs and target states: [Pt [Coffee] S0]
Input trace: [Button,Coin,Button,Coin,Button,Coin,Coin,Coin,Button]

Issue found in path 1, 0 paths executed, 0 paths truncated, in total 9 transitions.