From fe186011654050dff139d962b362a1b2846bc337 Mon Sep 17 00:00:00 2001 From: ajardin Date: Mon, 24 Nov 2025 11:30:28 +0100 Subject: [PATCH 1/2] example of set of different typed objects --- .../SetOperatorsExample7_no_ext.crml | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 src/test/resources/testModels/spec-doc-examples/SetOperatorsExample7_no_ext.crml diff --git a/src/test/resources/testModels/spec-doc-examples/SetOperatorsExample7_no_ext.crml b/src/test/resources/testModels/spec-doc-examples/SetOperatorsExample7_no_ext.crml new file mode 100644 index 0000000..60b9fec --- /dev/null +++ b/src/test/resources/testModels/spec-doc-examples/SetOperatorsExample7_no_ext.crml @@ -0,0 +1,24 @@ +model SetOperatorsExample7_no_ext is { + // extracting from a set of pieces of equipment + // the pieces of equipment that are in operation + class Equipment is { + String id; // Equipment identification + Boolean inOperation is external; // inOperation is true if the equipment is in operation + }; + + class Pump is { + extends Equipment; + String type = "Centrifugal"; + }; + + class Motor is { + extends Equipment; + String provider = "JohnDoe"; + }; + + Pump Equip1(id = "E1", inOperation = false); + Motor Equip2(id = "E2", inOperation = true); + Equipment Equip3(id = "E3", inOperation = true); + + Equipment {} S is filter { Equipment (id is "E1"), Equipment (id is "E2"), Equipment (id is "E3") } (element.inOperation == true); // S should be equal to {Equip2} +}; \ No newline at end of file From c5b9f6d34c222561c8297d49f2af62287eed1090 Mon Sep 17 00:00:00 2001 From: ajardin Date: Mon, 24 Nov 2025 15:49:39 +0100 Subject: [PATCH 2/2] example of recursive 'requirement' operator on sets --- .../FunctionalRequirements.crml | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 src/test/resources/testModels/spec-doc-examples/to_be_added_to_spec/FunctionalRequirements.crml diff --git a/src/test/resources/testModels/spec-doc-examples/to_be_added_to_spec/FunctionalRequirements.crml b/src/test/resources/testModels/spec-doc-examples/to_be_added_to_spec/FunctionalRequirements.crml new file mode 100644 index 0000000..83cda64 --- /dev/null +++ b/src/test/resources/testModels/spec-doc-examples/to_be_added_to_spec/FunctionalRequirements.crml @@ -0,0 +1,27 @@ +model FunctionalRequirements is { + + Operator [ Boolean ] 'decide' Boolean phi 'over' Period P = phi 'or' new Boolean (P end)); + Operator [ Boolean ] 'evaluate' Boolean phi 'over' Period P = integrate (('decide' phi 'over' P) * phi) on P; + Operator [ Boolean ] 'check' Boolean phi 'over' Periods P = and ({'evaluate' phi 'over' P.element}); + // and ({'evaluate' phi 'over' P.element}) + // = and( {'evaluate' phi 'over' P.e1, ..., 'evaluate' phi 'over' P.en} ) + // = 'evaluate over'(phi, P.e1) and ... and 'evaluate over'(phi, P.en) + // = fold( and, {'evaluate' phi 'over' P.element}) + // = fold( and, map( 'evaluate over', P)) + + Periods P1; + Periods P2; + + Boolean phi; + + Boolean R1 is 'check' phi 'over' P1; + Boolean R2 is 'check' phi 'over' P2; + Boolean R_on_all_periods is 'check' phi 'over' (P1 union P2); // Illegal (i.e. currently not defined) since Periods are not considered as typed set and 'union' operator is not defined for this specific type + Boolean R_on_all_periods2 is ('check' phi 'over' P1) and ('check' phi 'over' P2); // OK but a 'functional notation' would be preferable to be more concise + Boolean R_on_all_periods3 is 'check' phi 'over' {P1,P2}; // Should be equivalent to R_on_all_periods2 + // 'check' phi 'over' {P1,P2} + // = 'check over'(phi,{P1,P2}) + // = and( { 'evaluate over'( phi , {P1,P2}.element ) } ) + // = and( { 'evaluate over'( phi , P1.element ) }, { 'evaluate over'( phi , P2.element ) } ) + // = fold( 'check over', phi, {P1, P2} ) +}; \ No newline at end of file