Descriptions.tdltx

Package Descriptions {
  Import all from Standard
  Import all from Objectives
  Import all from Config
  Import all from generated_from_step3body_json
  Import all from generated_from_step2body_json
  Import all from HTTP.MessageBased
  Enumerated e1 {
  	e1 v1, 
  	v2 
  }
  
  
  Annotation Failure
  PICS xxx
  //introduce dedicated type that extends boolean?
//  Type ^PICS extends Boolean
//  PICS MW_8040
//  PICS MW_8345
  //or just annotated booleans? (probably more consistent):
  @PICS Boolean MW_8040
  @PICS Boolean MW_8345
  //TODO: add constraints for PICS guards?
  //TODO: make PICS a sub-type of simple data instance?
  
  
  Use "settings" as settings
  Map MW_8040 to "pics.mw_8040" in settings as MW_8040_MAPPING
  Map MW_8345 to "pics.mw_8345" in settings as MW_8345_MAPPING
  
  Boolean TD_SSP_01_Completed
  PICS MW_8345x 
  
  Test Purpose tpName {
      Objective: "description"
      Reference: "reference"
      PICS: MW_8345x and MW_8345x
  }

  //import   
  //@PICSs [ (MW_8040 or MW_8345) ] for testDescriptionName
  
  Test Description testDescriptionName    
    uses TestLanArchitecture  
//    if [ (MW_8040 or MW_8345) ] {
//      pm::mpi sends rGET() to X::mpi 
//      
//    }
  //TODO: annotation of behaviour or of block? (block in TPD) 
  //-> syntactically not possible to annotate block at the moment
  //-> even with exception, still assigned to behaviour
  //-> moved inside guard
    @PICS
    [ @PICS (MW_8040 or MW_8345) ] //if not true -> verdict N/A? test not executed
  {
    @Initial conditions {
       
    //-> aka preamble (postamble for final conditions)
    //if unexpected -> verdict inconclusive, map to junit annotations 
      perform action: "test"
      //pm::mpi sends rGET() to X::mpi 
    }
    //...
  }
  
  String modules_state_uri
  Use "pm.settings.json" as SETTINGS
  Map modules_state_uri 
    to "{{TD_SDN_RESTCONF_PATH}}/data/ietf-yang-library:modules-state" 
    in SETTINGS 
    as modules_state_uri_MAPPING

  //TODO:to be imported from protocol definition
  Structure JSON_modules_state extends Body (  
    String modules_state,
    Modules modules
  )
  
  JSON_modules_state JSON_instance_modules_state ()
  
  Collection Modules of Module
  Structure Module (
      String name,
      String revision,
      String namespace
  )
  

  // ...
  
  //TODO: clean up, align, document, and share 
  Test Description DomainControllerInitialisation uses TestLanArchitecture
  Test Description DomainControllersInitialisation uses TestLanArchitecture
  Test Description DevicesUpgrade uses TestLanArchitecture
  Test Description BasicConfigurationsSetup uses TestLanArchitecture
  Test Description L2DataServicesCreation uses TestLanArchitecture
  Test Description ResetDomainControllers uses TestLanArchitecture
  Test Description ResetMicrowaveUnits uses TestLanArchitecture
  
  Objective ResponseContainsAllYanModules {
  	Description: "The response body of the request should contain a list of all YANG modules"
  	References: "Postman implementation"
  }
  
  
  Test Purpose Description TPD_MDD_01 {
    Objective: TD_MDD_01
    Configuration: TestLanArchitecture //TREE_CFG?
    PICS: (MW_8040 or MW_8345) //etc.
    //TODO: add annotation to guard/expression to distinguish from regular guards? 
    //->turn PICS keyword into a annotation?
    
    
    Initial conditions  
    //TODO: do we need different semantics for unexpected behaviour within initial/final conditions? 
    //e.g. inconclusive instead of fail?
    //->in case describe in part 4/1
    with {
      //initial textual
      perform action: "Postman has been correctly initialized earlier, by executing 
                       TD_POSTMAN_INIT"
      perform action: "All the Domain Controller instances up and running normally"
      perform action: "All the devices are upgraded to correct versions"
      perform action: "All basic configurations are completed (e.g., NE_id, OSPF, PCEP, etc.)"
      //then gradually formalised, e.g.
      execute DomainControllersInitialisation 
      execute DevicesUpgrade
      execute BasicConfigurationsSetup
      //!DONE: check constraints above -> fixed
      //...
    }
    Expected behaviour
    ensure that {
      when {
        //initial textual
        perform action: "Send GET request via Postman to all domain controllers by 
                         executing Collection TD_MDD_01"
        //refine to first structure
        //TODO: what happens to all the parentheses?!?! -> make filter optional (or remove?)
        pm::mpi sends rGET() to X::mpi 
        //refine to specific uri inline 
        pm::mpi sends rGET(
          uri = "{{TD_SDN_RESTCONF_PATH}}/data/ietf-yang-library:modules-state"
        ) to X::mpi
        //...or define elsewhere
        pm::mpi sends rGET(
          uri = modules_state_uri
        ) to X::mpi
      }
      then {
        //initial textual
        perform action: "Check the response body of each request and confirm if all the 
                         Restconf servers are serviceable."
        perform action: "The response body of the request should contain a list of all 
                         YANG modules and submodules used by the Restconf server along with 
                         information about name and revision for each module."
        perform action: "The response body of each query should contain the specified YANG 
                         module along with its name and revision."

        //refinements
        // Test 1: Check the response body of the above request and confirm if the Restconf 
        // server is serviceable.
        pm::mpi receives OK() from X::mpi
        
        
        // Step 2: The response body of the request should contain a list of all YANG modules 
        //and submodules used by the Restconf server along with information about name and revision 
        //for each module.
        
        //---
        //asserts can be used but probably simpler to use a specification of the expected data
        //optionally: explicit objective that can be checked
        Objective: ResponseContainsAllYanModules
        pm::mpi receives OK(
            body = JSON_instance_modules_state(
              modules_state = ?,
              modules_state = ?, 
              //TODO: do we need a pattern ? / * for collections? Otherwise we need a loop instead
              //TODO: as a side note, is checking for the presence of a property 
              //      equivalent to that property having any value? 
              modules[*] = (name = ?, revision = ?, namespace = ?)  
              //...
        )) from X::mpi
        
        //asserts can provide fine granular diagnostics though, for individual problems
        response = pm::mpi receives OK() from X::mpi
        //optionally: explicit objective that can be checked
        Objective: ResponseContainsAllYanModules
        //optionally: annotations can be used for inline information
        @Failure: "The response body of the request should contain a list of all YANG modules"
        //TODO: property access for subclasses?
        //TODO: do we have matching expressions in assertions as well
        //TODO: do we have checking of types
        assert ( pm::response.body == JSON_instance_modules_state(
          modules_state = ?,
          //TODO: do we need a pattern ? / * for collections? Otherwise we need a loop instead
          //TODO: as a side note, is checking for the presence of a property 
          //      equivalent to that property having any value?
          modules[*] = (name = ?, revision = ?, namespace = ?)
          // 
        )) 
          on pm //may be skipped at first 
          with {
            timeLabel=now
          }
        
        //alternatively with a loop
        //TODO: do we need counters? integrated in loops? e.g. with state to address collections?
        pm::i = 0
        repeat 5 times on pm 
        //[MW_8040]
        { 
          //DONE: fixed constraint with bounded loop behaviour, still not quite there
          assert ( pm::response.body == JSON_instance_modules_state(
            modules_state = ?,
            //TODO: as a side note, is checking for the presence of a property 
            //      equivalent to that property having any value?
            modules[pm::i] = (name = ?, revision = ?, namespace = ?)
            // 
          )) 
            on pm //may be skipped at first 
          //DONE: handle undefined return types -> a bit of a hack, assuming they are the same
          pm::i = ( pm::i + 1 )
        } 
      }
    }
  }
  
  
  
  
   Test Purpose Description TPD_MSP_01 {
    Objective: TD_MSP_01
    Configuration: TestLanArchitecture //TREE_CFG?
    PICS: (MW_8040 or MW_8345) //etc.
    Initial conditions
    with {
      //initial textual
      perform action: "Postman has been correctly initialized earlier, by executing TD_POSTMAN_INIT"
      perform action: "The Domain Controller instance is up and running normally"
      perform action: "All the devices are upgraded to correct versions"
      perform action: "All basic configurations are completed (e.g., NE_id, OSPF, PCEP, etc.)"
      perform action: "All Restconf servers are serviceable."
      perform action: "If TD_SSP_01 has been run before TD_ MSP_01, all Domain Controllers and 
                       microwave units should be reset to the state they were before executing 
                       TD_SSP_01"
      //then gradually formalised, e.g.
      execute DomainControllerInitialisation 
      execute DomainControllerInitialisation 
      execute DevicesUpgrade
      execute BasicConfigurationsSetup
      if [TD_SSP_01_Completed] {
        execute ResetDomainControllers
        execute ResetMicrowaveUnits
      }
      //!TODO: check constraints above
      //...
    }
    Expected behaviour
    ensure that {
      when {
        //initial textual
        perform action: "Send POST request via Postman to all domain controllers 
                         by executing Collection TD_ SSP_01"
//        //refine to first structure
//        pm::mpi sends rPOST() to X::mpi
//        //refine to specific body (or define inline)
//        pm::mpi sends rPOST(body = JSON_instance) to X::mpi
//           
//        //provide additional parameter overrides 
//        pm::mpi sends rPOST(
//          body = JSON_instance ( 
//            services[0].adminStatus = "up",
//            //..
//            //TODO: check constraints
//            services[0].ports[1].accessNodeId = node1
//            //..
//          )
//        )
//        to X::mpi //....
      }
      then {
        //initial textual
        perform action: "Check the TGA if the data start flowing properly."
//        pm::mpi receives OK() from X::mpi
//        pm::mpi receives OK(body = JSON_instance) from X::mpi
//        pm::mpi receives OK(
//          body = JSON_instance(
//            //..
//            services[2] = omit,
//            //...
//            services[3].ports[1] = omit
//          )
//        ) 
//        from X::mpi
//        //first response definition, then refined, also with overrides
//        //!TODO: Why are comments before receive message not OK?
//        //... refine further
      }
    }
  }
 
 
  
  Test Purpose Description TPD_MSP_04 {
    Objective: TD_MSP_04
    Configuration: TestLanArchitecture //TREE_CFG?
    PICS: (MW_8040 or MW_8345) //etc.
    Initial conditions
    with {
      //initial textual
      perform action: "Postman has been correctly initialized earlier, by executing TD_POSTMAN_INIT"
      perform action: "All the Domain Controller instances are up and running normally"
      perform action: "All the devices are upgraded to correct versions"
      perform action: "All basic configurations are completed (e.g., NE_id, OSPF, PCEP, etc.)"
      perform action: "All Restconf servers are serviceable."
      perform action: "All L2 data services are successfully created."
      //then gradually formalised, e.g.
      execute DomainControllersInitialisation
      execute DevicesUpgrade
      execute BasicConfigurationsSetup
      execute L2DataServicesCreation
      //!TODO: check constraints above
      //...
    }
    Expected behaviour
    ensure that {
      when {
        //initial textual
        perform action: "Send GET request via Postman to 
                all domain controllers by executing 
                Collection TD_MSP_04"
        //refine to first structure
        pm::mpi sends rGET() to X::mpi
        //refine to specific body (or define inline)
        pm::mpi sends rGET(body = JSON_instance) to X::mpi
         
        //provide additional parameter overrides 
        pm::mpi sends rGET(
          body = JSON_instance ( 
            services[0].adminStatus = "up" {JSON_String},
            //..
            //DONE: check constraints
            services[0].ports[1].accessNodeId = node1
            //..
          )
        )
        to X::mpi //....
      }
      then {
        //initial textual
        perform action: "The response body should no longer contain 
                 information about the L2 service deleted in TD_MSP_03"
        //!DONE: Why are comments before receive message not OK? -> fixed
        //basic response definition 
        pm::mpi receives OK() from X::mpi
        //refined with reference to body definition
        pm::mpi receives OK(body = JSON_instance) from X::mpi
        //refined with inline overrides
        pm::mpi receives OK(
          body = JSON_instance(
            //..
            //TODO: does an optional collection member imply entire collection is ommitted?
            //      or also individual items?
            //TODO: does special value use conform to everything?
            services[2] = omit,
            //...
            services[3].ports[1] = omit
          )
        ) 
        from X::mpi
        //... refine further
      }
    }
  }
  
}