demo/SpecExplorer/Project/MBT_SIP/Model/Config.cord

// This is a Spec Explorer coordination script (Cord version 1.0).
// Here is where you define configurations and machines describing the
// exploration to be performed.

using MBT.Adapter; 

/// Contains actions of the model, bounds, and switches.
config Main 
{    
    action abstract static void Adapter.start();    
    action abstract static void Adapter.end();
    action abstract static void Adapter.Init_Calling();
    action abstract static void Adapter.Calling_Ringing();
    action abstract static void Adapter.Calling_Timeout();
    action abstract static void Adapter.Ringing_Canceling();
    action abstract static void Adapter.Ringing_Ready();
    action abstract static void Adapter.Ringing_Reject();
    action abstract static void Adapter.Canceling_WaitingResponse();
    action abstract static void Adapter.Canceling_Timeout();
    action abstract static void Adapter.WaitingResponse_Terminate();
    action abstract static void Adapter.Ready_Terminating();
    action abstract static void Adapter.Ready_End();
    action abstract static void Adapter.Terminating_OK();
    action abstract static void Adapter.Terminating_Timeout();

    switch StepBound = 1024;
    switch PathDepthBound = 1024;
    switch StateBound = 1024;
    switch TestClassBase = "vs";
    switch GeneratedTestPath = "..\\TestSuite";
    switch GeneratedTestNamespace = "MBT.TestSuite";
    switch TestEnabled = false;
    switch ForExploration = false;
}

machine Model() : Main where ForExploration = true
{
    Model_CLOSED_START()*
}

machine Model_CLOSED_START() : Main
{
    start() ; (( Init_Calling() ; Model_Calling() ) | ( Calling_Timeout() ; Model_CLOSED_END() ) )
}

machine Model_Calling() : Main
{
    ( Calling_Ringing() ; Model_Ringing() )
}

machine Model_Ringing() : Main
{
    ( Ringing_Canceling() ; Model_Canceling() ) | ( Ringing_Ready() ; Model_Ready() ) | ( Ringing_Reject() ; Model_CLOSED_END() ) | ( Canceling_Timeout() ; Model_CLOSED_END() )
}

machine Model_Canceling() : Main
{
    ( Canceling_WaitingResponse() ; Model_WaitingResponse() )
}

machine Model_Ready() : Main
{
   ( Ready_Terminating() ; Model_Terminating() ) | ( Ready_End() ; Model_CLOSED_END() ) | ( Terminating_Timeout() ; Model_CLOSED_END() )
}

machine Model_Terminating() : Main
{
    ( Terminating_OK() ; Model_CLOSED_END() )
}

machine Model_WaitingResponse() : Main
{
    ( WaitingResponse_Terminate() ; Model_CLOSED_END() )
}


machine Model_CLOSED_END() : Main
{
    end()
}

machine ModelProgram() : Main
{
    construct model program from Main
    where namespace = "MBT.Model" 
}

machine Model_Sync() : Main where ForExploration = true
{
    Model || ModelProgram
}

machine Testsuite() : Main where ForExploration = true, TestEnabled = true
{    
    construct test cases
        where AllowUndeterminedCoverage = true
    for Model_Sync
}