810 lines
23 KiB
Plaintext
810 lines
23 KiB
Plaintext
// Source-only fixture: validation and native acceptance have NOT been executed.
|
|
// Preserve this comment and Unicode Ω, 戻り値, é and 👩🔧 during save/reopen.
|
|
arcadia 7;
|
|
project lifecycle_native "Nested lifecycle union acceptance" id "21c0fe00-0000-4000-8000-000000000001" {
|
|
description "Six compact scenarios for typed activations, birth/death, long labels and admitted incomplete paths. Fixture preparation is source review only; run preflight before native acceptance.";
|
|
|
|
oa_activity bound_100 "Review pressure demand" id "21c0fe00-0000-4000-8000-000000000064" {
|
|
description "";
|
|
parent none;
|
|
}
|
|
|
|
oa_activity bound_101 "WWWWWWWWWWWWWWWWWW pressure inspection activity" id "21c0fe00-0000-4000-8000-000000000065" {
|
|
description "";
|
|
parent none;
|
|
}
|
|
|
|
oa_exchange_item bound_110 "Check pressure" id "21c0fe00-0000-4000-8000-00000000006e" {
|
|
description "";
|
|
kind Information;
|
|
mechanism Operation;
|
|
parent none;
|
|
supertype none;
|
|
}
|
|
|
|
oa_data_field bound_111 "requested_pressure" id "21c0fe00-0000-4000-8000-00000000006f" {
|
|
default none;
|
|
description "";
|
|
direction In;
|
|
maximum 1;
|
|
minimum 1;
|
|
parent @bound_110;
|
|
storage Value;
|
|
type_ref Real;
|
|
unit "kPa";
|
|
}
|
|
|
|
oa_data_field bound_112 "measured_pressure" id "21c0fe00-0000-4000-8000-000000000070" {
|
|
default none;
|
|
description "";
|
|
direction Return;
|
|
maximum 1;
|
|
minimum 1;
|
|
parent @bound_110;
|
|
storage Value;
|
|
type_ref Real;
|
|
unit "kPa";
|
|
}
|
|
|
|
interaction bound_120 "Pressure check" id "21c0fe00-0000-4000-8000-000000000078" {
|
|
description "";
|
|
items [@bound_110];
|
|
source @bound_100;
|
|
target @bound_101;
|
|
}
|
|
|
|
sa_actor bound_200 "Operator console" id "21c0fe00-0000-4000-8000-0000000000c8" {
|
|
description "";
|
|
parent none;
|
|
}
|
|
|
|
sa_system bound_201 "界界界界界界界界界界界界 圧力確認サービス 👩🔧" id "21c0fe00-0000-4000-8000-0000000000c9" {
|
|
description "";
|
|
parent none;
|
|
}
|
|
|
|
sa_port bound_202 "Client socket" id "21c0fe00-0000-4000-8000-0000000000ca" {
|
|
contract {
|
|
Component {
|
|
kind Standard;
|
|
orientation Unset;
|
|
};
|
|
};
|
|
description "";
|
|
legacy none;
|
|
parent @bound_200;
|
|
}
|
|
|
|
sa_port bound_203 "Service socket" id "21c0fe00-0000-4000-8000-0000000000cb" {
|
|
contract {
|
|
Component {
|
|
kind Standard;
|
|
orientation Unset;
|
|
};
|
|
};
|
|
description "";
|
|
legacy none;
|
|
parent @bound_201;
|
|
}
|
|
|
|
sa_exchange_item bound_210 "Check pressure" id "21c0fe00-0000-4000-8000-0000000000d2" {
|
|
description "";
|
|
kind Information;
|
|
mechanism Operation;
|
|
parent none;
|
|
supertype none;
|
|
}
|
|
|
|
sa_data_field bound_211 "requested_pressure" id "21c0fe00-0000-4000-8000-0000000000d3" {
|
|
default none;
|
|
description "";
|
|
direction In;
|
|
maximum 1;
|
|
minimum 1;
|
|
parent @bound_210;
|
|
storage Value;
|
|
type_ref Real;
|
|
unit "kPa";
|
|
}
|
|
|
|
sa_data_field bound_212 "measured_pressure" id "21c0fe00-0000-4000-8000-0000000000d4" {
|
|
default none;
|
|
description "";
|
|
direction Return;
|
|
maximum 1;
|
|
minimum 1;
|
|
parent @bound_210;
|
|
storage Value;
|
|
type_ref Real;
|
|
unit "kPa";
|
|
}
|
|
|
|
sa_interface bound_213 "Pressure check API" id "21c0fe00-0000-4000-8000-0000000000d5" {
|
|
description "";
|
|
parent none;
|
|
supertype none;
|
|
}
|
|
|
|
interface_item_allocation bound_220 "Synchronous pressure check" id "21c0fe00-0000-4000-8000-0000000000dc" {
|
|
acquisition Unspecified;
|
|
description "";
|
|
order 0;
|
|
source @bound_213;
|
|
target @bound_210;
|
|
transmission Synchronous;
|
|
}
|
|
|
|
interface_requirement bound_221 "Console requires check" id "21c0fe00-0000-4000-8000-0000000000dd" {
|
|
description "";
|
|
source @bound_202;
|
|
target @bound_213;
|
|
}
|
|
|
|
interface_provision bound_222 "Service provides check" id "21c0fe00-0000-4000-8000-0000000000de" {
|
|
description "";
|
|
source @bound_203;
|
|
target @bound_213;
|
|
}
|
|
|
|
boundary_exchange bound_223 "Pressure channel" id "21c0fe00-0000-4000-8000-0000000000df" {
|
|
description "";
|
|
items [@bound_210];
|
|
oriented false;
|
|
source @bound_202;
|
|
target @bound_203;
|
|
}
|
|
|
|
oa_scenario bound_1000 "OA 1 Nested lifetime — Latin" id "21c0fe00-0000-4000-8000-0000000003e8" {
|
|
context none;
|
|
description "";
|
|
parent none;
|
|
postcondition "Each reply retains its own requested and measured values";
|
|
precondition "Two pressure checks are reviewed before the outer reply";
|
|
steps [@bound_1005, @bound_1040, @bound_1030, @bound_1060, @bound_1050, @bound_1070];
|
|
viewpoint OperationalActivity;
|
|
}
|
|
|
|
oa_lifeline bound_1001 "L1 Console" id "21c0fe00-0000-4000-8000-0000000003e9" {
|
|
description "";
|
|
parent @bound_1000;
|
|
represented @bound_100;
|
|
}
|
|
|
|
oa_lifeline bound_1002 "L2 WWWWWWWWWWWWWWWWWW Inspector" id "21c0fe00-0000-4000-8000-0000000003ea" {
|
|
description "";
|
|
parent @bound_1000;
|
|
represented @bound_101;
|
|
}
|
|
|
|
oa_occurrence bound_1005 "Create inspector" id "21c0fe00-0000-4000-8000-0000000003ed" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Create;
|
|
receiver @bound_1002;
|
|
reply_to none;
|
|
sender @bound_1001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_1000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_1030 "C2 380 kPa" id "21c0fe00-0000-4000-8000-000000000406" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_120;
|
|
message_kind Call;
|
|
receiver @bound_1002;
|
|
reply_to none;
|
|
sender @bound_1001;
|
|
values [{
|
|
expression "380.0";
|
|
field @bound_111;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_1000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_1040 "C1 420 kPa" id "21c0fe00-0000-4000-8000-000000000410" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_120;
|
|
message_kind Call;
|
|
receiver @bound_1002;
|
|
reply_to none;
|
|
sender @bound_1001;
|
|
values [{
|
|
expression "420.0";
|
|
field @bound_111;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_1000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_1050 "R1 418 kPa" id "21c0fe00-0000-4000-8000-00000000041a" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_120;
|
|
message_kind Reply;
|
|
receiver @bound_1001;
|
|
reply_to @bound_1040;
|
|
sender @bound_1002;
|
|
values [{
|
|
expression "418.0";
|
|
field @bound_112;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_1000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_1060 "R2 378 kPa" id "21c0fe00-0000-4000-8000-000000000424" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_120;
|
|
message_kind Reply;
|
|
receiver @bound_1001;
|
|
reply_to @bound_1030;
|
|
sender @bound_1002;
|
|
values [{
|
|
expression "378.0";
|
|
field @bound_112;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_1000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_1070 "Delete inspector" id "21c0fe00-0000-4000-8000-00000000042e" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Delete;
|
|
receiver @bound_1002;
|
|
reply_to none;
|
|
sender @bound_1001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_1000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_scenario bound_2000 "SA 2 Nested lifetime — Unicode" id "21c0fe00-0000-4000-8000-0000000007d0" {
|
|
context none;
|
|
description "";
|
|
parent none;
|
|
postcondition "Each reply retains its own requested and measured values";
|
|
precondition "Two pressure checks are reviewed before the outer reply";
|
|
steps [@bound_2005, @bound_2040, @bound_2030, @bound_2060, @bound_2050, @bound_2070];
|
|
viewpoint BoundaryInterface;
|
|
}
|
|
|
|
sa_lifeline bound_2001 "L1 Console" id "21c0fe00-0000-4000-8000-0000000007d1" {
|
|
description "";
|
|
parent @bound_2000;
|
|
represented @bound_200;
|
|
}
|
|
|
|
sa_lifeline bound_2002 "L2 界界界界界界界界界界界界 戻り値 👩🔧" id "21c0fe00-0000-4000-8000-0000000007d2" {
|
|
description "";
|
|
parent @bound_2000;
|
|
represented @bound_201;
|
|
}
|
|
|
|
sa_occurrence bound_2005 "Create inspector" id "21c0fe00-0000-4000-8000-0000000007d5" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Create;
|
|
receiver @bound_2002;
|
|
reply_to none;
|
|
sender @bound_2001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_2000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_2030 "C2 380 kPa" id "21c0fe00-0000-4000-8000-0000000007ee" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_223;
|
|
message_kind Call;
|
|
operation {
|
|
allocation @bound_220;
|
|
};
|
|
receiver @bound_2002;
|
|
reply_to none;
|
|
sender @bound_2001;
|
|
values [{
|
|
expression "380.0";
|
|
field @bound_211;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_2000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_2040 "C1 420 kPa" id "21c0fe00-0000-4000-8000-0000000007f8" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_223;
|
|
message_kind Call;
|
|
operation {
|
|
allocation @bound_220;
|
|
};
|
|
receiver @bound_2002;
|
|
reply_to none;
|
|
sender @bound_2001;
|
|
values [{
|
|
expression "420.0";
|
|
field @bound_211;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_2000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_2050 "R1 418 kPa" id "21c0fe00-0000-4000-8000-000000000802" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_223;
|
|
message_kind Reply;
|
|
receiver @bound_2001;
|
|
reply_to @bound_2040;
|
|
sender @bound_2002;
|
|
values [{
|
|
expression "418.0";
|
|
field @bound_212;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_2000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_2060 "R2 378 kPa" id "21c0fe00-0000-4000-8000-00000000080c" {
|
|
body {
|
|
Exchange {
|
|
exchange @bound_223;
|
|
message_kind Reply;
|
|
receiver @bound_2001;
|
|
reply_to @bound_2030;
|
|
sender @bound_2002;
|
|
values [{
|
|
expression "378.0";
|
|
field @bound_212;
|
|
path [];
|
|
}];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_2000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_2070 "Delete inspector" id "21c0fe00-0000-4000-8000-000000000816" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Delete;
|
|
receiver @bound_2002;
|
|
reply_to none;
|
|
sender @bound_2001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_2000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_scenario bound_3000 "OA 3 Self lifecycle and call" id "21c0fe00-0000-4000-8000-000000000bb8" {
|
|
context none;
|
|
description "Native lifecycle union acceptance fixture; completeness warnings are intentional.";
|
|
parent none;
|
|
postcondition "";
|
|
precondition "";
|
|
steps [@bound_3010, @bound_3020, @bound_3040, @bound_3050, @bound_3070];
|
|
viewpoint OperationalActivity;
|
|
}
|
|
|
|
oa_lifeline bound_3001 "L1 Creator" id "21c0fe00-0000-4000-8000-000000000bb9" {
|
|
description "";
|
|
parent @bound_3000;
|
|
represented @bound_100;
|
|
}
|
|
|
|
oa_lifeline bound_3002 "L2 自己検査 é é é 👩🔧 確認担当" id "21c0fe00-0000-4000-8000-000000000bba" {
|
|
description "";
|
|
parent @bound_3000;
|
|
represented @bound_101;
|
|
}
|
|
|
|
oa_occurrence bound_3010 "Prepare creation" id "21c0fe00-0000-4000-8000-000000000bc2" {
|
|
body {
|
|
Action {
|
|
action @bound_100;
|
|
lifeline @bound_3001;
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_3000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_3020 "Self create" id "21c0fe00-0000-4000-8000-000000000bcc" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Create;
|
|
receiver @bound_3002;
|
|
reply_to none;
|
|
sender @bound_3002;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_3000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_3040 "Self call" id "21c0fe00-0000-4000-8000-000000000be0" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Call;
|
|
receiver @bound_3002;
|
|
reply_to none;
|
|
sender @bound_3002;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_3000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_3050 "Self reply" id "21c0fe00-0000-4000-8000-000000000bea" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Reply;
|
|
receiver @bound_3002;
|
|
reply_to @bound_3040;
|
|
sender @bound_3002;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_3000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_3070 "Self delete" id "21c0fe00-0000-4000-8000-000000000bfe" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Delete;
|
|
receiver @bound_3002;
|
|
reply_to none;
|
|
sender @bound_3002;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_3000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_scenario bound_4000 "OA 4 Death in one ALT operand" id "21c0fe00-0000-4000-8000-000000000fa0" {
|
|
context none;
|
|
description "Native lifecycle union acceptance fixture; completeness warnings are intentional.";
|
|
parent none;
|
|
postcondition "";
|
|
precondition "";
|
|
steps [@bound_4040, @bound_4080];
|
|
viewpoint OperationalActivity;
|
|
}
|
|
|
|
oa_lifeline bound_4001 "L1 Requester" id "21c0fe00-0000-4000-8000-000000000fa1" {
|
|
description "";
|
|
parent @bound_4000;
|
|
represented @bound_100;
|
|
}
|
|
|
|
oa_lifeline bound_4002 "L2 Conditional inspector" id "21c0fe00-0000-4000-8000-000000000fa2" {
|
|
description "";
|
|
parent @bound_4000;
|
|
represented @bound_101;
|
|
}
|
|
|
|
oa_occurrence bound_4040 "Unanswered call" id "21c0fe00-0000-4000-8000-000000000fc8" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Call;
|
|
receiver @bound_4002;
|
|
reply_to none;
|
|
sender @bound_4001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_4000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_4070 "Delete without reply" id "21c0fe00-0000-4000-8000-000000000fe6" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Delete;
|
|
receiver @bound_4002;
|
|
reply_to none;
|
|
sender @bound_4001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_4081;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_4080 "Delete or keep alive" id "21c0fe00-0000-4000-8000-000000000ff0" {
|
|
body {
|
|
Fragment {
|
|
operator Alternative;
|
|
branches [@bound_4081, @bound_4082];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_4000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_4081 "Delete path" id "21c0fe00-0000-4000-8000-000000000ff1" {
|
|
body {
|
|
Branch {
|
|
guard "shutdown";
|
|
occurrences [@bound_4070];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_4080;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
oa_occurrence bound_4082 "Open path" id "21c0fe00-0000-4000-8000-000000000ff2" {
|
|
body {
|
|
Branch {
|
|
guard "continue";
|
|
occurrences [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_4080;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_scenario bound_5000 "SA 5 Death and incomplete reply" id "21c0fe00-0000-4000-8000-000000001388" {
|
|
context none;
|
|
description "Native lifecycle union acceptance fixture; completeness warnings are intentional.";
|
|
parent none;
|
|
postcondition "";
|
|
precondition "";
|
|
steps [@bound_5040, @bound_5070, @bound_5050];
|
|
viewpoint BoundaryInterface;
|
|
}
|
|
|
|
sa_lifeline bound_5001 "L1 Requester" id "21c0fe00-0000-4000-8000-000000001389" {
|
|
description "";
|
|
parent @bound_5000;
|
|
represented @bound_200;
|
|
}
|
|
|
|
sa_lifeline bound_5002 "L2 Terminated service" id "21c0fe00-0000-4000-8000-00000000138a" {
|
|
description "";
|
|
parent @bound_5000;
|
|
represented @bound_201;
|
|
}
|
|
|
|
sa_occurrence bound_5040 "Unanswered call" id "21c0fe00-0000-4000-8000-0000000013b0" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Call;
|
|
receiver @bound_5002;
|
|
reply_to none;
|
|
sender @bound_5001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_5000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_5050 "Incomplete reply — no sender" id "21c0fe00-0000-4000-8000-0000000013ba" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Reply;
|
|
receiver @bound_5001;
|
|
reply_to @bound_5040;
|
|
sender none;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_5000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_5070 "Delete service" id "21c0fe00-0000-4000-8000-0000000013ce" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Delete;
|
|
receiver @bound_5002;
|
|
reply_to none;
|
|
sender @bound_5001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_5000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_scenario bound_6000 "SA 6 Unresolved lifetime, visible cue" id "21c0fe00-0000-4000-8000-000000001770" {
|
|
context none;
|
|
description "Native lifecycle union acceptance fixture; completeness warnings are intentional.";
|
|
parent none;
|
|
postcondition "";
|
|
precondition "";
|
|
steps [@bound_6080];
|
|
viewpoint BoundaryInterface;
|
|
}
|
|
|
|
sa_lifeline bound_6001 "L1 Requester" id "21c0fe00-0000-4000-8000-000000001771" {
|
|
description "";
|
|
parent @bound_6000;
|
|
represented @bound_200;
|
|
}
|
|
|
|
sa_lifeline bound_6002 "L2 Unresolved service" id "21c0fe00-0000-4000-8000-000000001772" {
|
|
description "";
|
|
parent @bound_6000;
|
|
represented @bound_201;
|
|
}
|
|
|
|
sa_occurrence bound_6005 "Create service" id "21c0fe00-0000-4000-8000-000000001775" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Create;
|
|
receiver @bound_6002;
|
|
reply_to none;
|
|
sender @bound_6001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_6081;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_6040 "Call with unresolved lifetime" id "21c0fe00-0000-4000-8000-000000001798" {
|
|
body {
|
|
Exchange {
|
|
exchange none;
|
|
message_kind Call;
|
|
receiver @bound_6002;
|
|
reply_to none;
|
|
sender @bound_6001;
|
|
values [];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_6082;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_6080 "Birth is path dependent" id "21c0fe00-0000-4000-8000-0000000017c0" {
|
|
body {
|
|
Fragment {
|
|
operator Alternative;
|
|
branches [@bound_6081, @bound_6082];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_6000;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_6081 "Create path" id "21c0fe00-0000-4000-8000-0000000017c1" {
|
|
body {
|
|
Branch {
|
|
guard "start new";
|
|
occurrences [@bound_6005];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_6080;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
|
|
sa_occurrence bound_6082 "Call path" id "21c0fe00-0000-4000-8000-0000000017c2" {
|
|
body {
|
|
Branch {
|
|
guard "use existing";
|
|
occurrences [@bound_6040];
|
|
};
|
|
};
|
|
description "";
|
|
parent @bound_6080;
|
|
postcondition "";
|
|
precondition "";
|
|
}
|
|
}
|
|
|