From 725a7d35f1c54f79d29670d1a41b8a9e979b72e4 Mon Sep 17 00:00:00 2001 From: Philip Makedonski <makedonski@informatik.uni-goettingen.de> Date: Wed, 24 Jan 2024 15:24:58 +0100 Subject: [PATCH] + updated MWT examples (WIP) --- mwt-examples/src/tdl/Config.tdltx | 2 +- mwt-examples/src/tdl/Data.tdltx | 6 ++- mwt-examples/src/tdl/Descriptions.tdltx | 21 ++++++--- mwt-examples/src/tdl/acme.yang | 47 +++++++++++++++++++ .../src/tdl/acme.yang-generated.tdltx | 22 +++++++++ 5 files changed, 89 insertions(+), 9 deletions(-) create mode 100644 mwt-examples/src/tdl/acme.yang create mode 100644 mwt-examples/src/tdl/acme.yang-generated.tdltx diff --git a/mwt-examples/src/tdl/Config.tdltx b/mwt-examples/src/tdl/Config.tdltx index 370f692..c4fc4fe 100644 --- a/mwt-examples/src/tdl/Config.tdltx +++ b/mwt-examples/src/tdl/Config.tdltx @@ -6,7 +6,7 @@ Package Config { Import all from HTTP Import all from HTTP.MessageBased Import all from generated_from_step3body_json - Import all from generated_from_step2body_json + Import all from generated_from_step2body_json //example type Type float //define additional elements here diff --git a/mwt-examples/src/tdl/Data.tdltx b/mwt-examples/src/tdl/Data.tdltx index 215c0ee..1d6daf4 100644 --- a/mwt-examples/src/tdl/Data.tdltx +++ b/mwt-examples/src/tdl/Data.tdltx @@ -2,6 +2,8 @@ * This is an example model */ Package Data { - - + Enumerated e1 { + e1 v1, + v2 + } } diff --git a/mwt-examples/src/tdl/Descriptions.tdltx b/mwt-examples/src/tdl/Descriptions.tdltx index a81ce23..775cc52 100644 --- a/mwt-examples/src/tdl/Descriptions.tdltx +++ b/mwt-examples/src/tdl/Descriptions.tdltx @@ -5,6 +5,11 @@ Package Descriptions { 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 @@ -35,8 +40,8 @@ Package Descriptions { //import //@PICSs [ (MW_8040 or MW_8345) ] for testDescriptionName - Test Description testDescriptionName - uses TestLanArchitecture + Test Description testDescriptionName + uses TestLanArchitecture // if [ (MW_8040 or MW_8345) ] { // pm::mpi sends rGET() to X::mpi // @@ -45,13 +50,15 @@ Package Descriptions { //-> syntactically not possible to annotate block at the moment //-> even with exception, still assigned to behaviour //-> moved inside guard -// @PICS + @PICS [ @PICS (MW_8040 or MW_8345) ] //if not true -> verdict N/A? test not executed { - @Initial conditions { + @Initial conditions { + //-> aka preamble (postamble for final conditions) //if unexpected -> verdict inconclusive, map to junit annotations - pm::mpi sends rGET() to X::mpi + perform action: "test" + //pm::mpi sends rGET() to X::mpi } //... } @@ -64,7 +71,7 @@ Package Descriptions { as modules_state_uri_MAPPING //TODO:to be imported from protocol definition - Structure JSON_modules_state extends Body ( + Structure JSON_modules_state extends Body ( String modules_state, Modules modules ) @@ -102,6 +109,8 @@ Package Descriptions { 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? diff --git a/mwt-examples/src/tdl/acme.yang b/mwt-examples/src/tdl/acme.yang new file mode 100644 index 0000000..197595e --- /dev/null +++ b/mwt-examples/src/tdl/acme.yang @@ -0,0 +1,47 @@ +// Contents of "acme-system.yang" +module acme-system { + namespace "http://acme.example.com/system"; + prefix "acme"; + + organization "ACME Inc."; + contact "joe@acme.example.com"; + description + "The module for entities implementing the ACME system."; + + revision 2007-06-09 { + description "Initial revision."; + } + + container system { + leaf host-name { + type string; + description "Hostname for this system"; + } + + leaf-list domain-search { + type string; + description "List of domain names to search"; + } + + container login { + leaf message { + type string; + description + "Message given at start of login session"; + } + + list user { + key "name"; + leaf name { + type string; + } + leaf full-name { + type string; + } + leaf class { + type string; + } + } + } + } +} \ No newline at end of file diff --git a/mwt-examples/src/tdl/acme.yang-generated.tdltx b/mwt-examples/src/tdl/acme.yang-generated.tdltx new file mode 100644 index 0000000..35a3f34 --- /dev/null +++ b/mwt-examples/src/tdl/acme.yang-generated.tdltx @@ -0,0 +1,22 @@ +Package generated_from_acme_yang { + Type String + Type TODO_RESOLVE_REFERENCED + Use "acme.yang" as SOURCE_MAPPING + Structure system ( + string host_name, + string_collection domain_search, + system___login login + ) + Type string + Collection string_collection of string + Structure system___login ( + string message, + login___user_collection user + ) + Structure login___user ( + string ^name, + string full_name, + string class + ) + Collection login___user_collection of login___user +} \ No newline at end of file -- GitLab