Running the IOCO Checker in JTorX

  1. Enter the path to the specification file in Config Items text field Model
    (or use the Browse button; make sure it shows All supported Formats)
  2. Enter the path to the implementation (model) file in Config Items text field Implementation
  3. Select the Interpretation that is right for your specification and implementation models
  4. Select traces kind: Straces or Utraces.
  5. Select the iocoCheck tab.
  6. Press the Check button, after a while results will be presented.
  7. You will have to look at the results by hand, or use them as guidance
  8. To run a Guided Test:
    1. Select one of the iocoChecker result lines.
    2. Enable guided testing by pressing the Guide check-button in the Config Items pane.
    3. Choose the guidance kind: use selected iocoChecker trace, or use combination of all iocoChecker traces
    4. Select the Test tab.
    5. Optionally, choose your own random number Seed.
    6. Press the Start button - it will show Stop, and a Log pane will appear.
    7. Use the buttons in the Next test step(s) pane to execute test steps -- typically you will use the Auto button in this case.
    8. If the simulation keeps running, press the Stop button when you are done.
    9. You may want to close the Log panes when you are done.

Notes

  1. ability to stop a long run was added in v1.3.0.
  2. make sure that your model and implementation do not contain tau-loops (loops of only internal steps), or else iocoChecker will try to run forever.

Back to Usage scenarios