Howto: Realizability Checking

This page presents how to use SChorA to check the realizability of a choreography specification spec. You need follow the steps bellow:

  1. goto SChorA IDE:
  2. click on New button to create a new SChorA script
  3. enter the models of spec after DECLARATIONS keyword. The model is put into component and end component keywords. For example:
        component impl chorD
            request[a,b] ; response[b,a]
        end component
  4. enter a command to check realizability of spec after COMMANDS keyword. For example
        showRealizableSTG spec SYNC

    This command will check the realizability of spec under synchronous communication. For other communication mode, you can use one of follow: ASYNC_SENDER, ASYNC_RECEIVER or ASYNC_DISJOINT

  5. click on button Run to execute the script
  6. the result is display on Output tab.

Last modified: July 10, 2013