Embedded Files
| # | Invariants |
| 1 | Requirement A1: Migration Costs Cumulated: Eager > Lazy, i.e. the graph of the strategy Eager is greater than the graph of the strategy Lazy throughout all releases.
| 2 | Tendency A2: Migration Costs Cumulated: Eager > x > Lazy, i.e. the graph of the strategy Eager equals the upper bound and the graph of the strategy Lazy equals the lower bound throughout all releases.
| 3 | Requirement A3: Migration Costs On-read: Eager == 0 <= x, i.e. the graph of the strategy Eager is always zero, even more so the Eager graph is below every other graph x.
| 4 | Requirement A4: Migration Costs On-release: Lazy == 0 < x, i.e. the graph of the strategy Lazy is always zero, even more so the Lazy graph is strictly below every other graph x.
| 5 | Tendency A5: Latency per entity access: Eager < x < Lazy, i.e. the graph of the strategy Eager equals the lower bound and the graph of the strategy Lazy equals the upper bound throughout all releases; all other graphs are located in between.
| 6 | Anforderung A6: Migration Debt: Eager == 0 <= x, d.h. der Graph der Strategie Eager ist immer Null, insbesondere liegt er immer unterhalb jedes anderen Graphen x.
| 6 | Requirement A6: Migration Debt: Eager == 0 <= x, i.e. the graph of the strategy Eager is always zero, even more so the Eager graph is below every other graph x.
| 7 | Requirement B1: Migration Costs Cumulated == Sum(MC On-read deltas + MC On-release deltas), i.e. for every strategy holds that the Migration Costs Cumulated are equal to the sum of Migration Costs On-read + On-release throughout all releases.
| 8 | Tendency B2: Incremental: It holds for all releases of the Incremental strategy that wherever the Migration Costs On-release have a local maximum that release the Migration Debt is zero.
| 9 | Tendency B3: Latency per Entity Access proportional Migration Costs On-read: The lower the Migration Costs On-release, the lower are the latency times.
| 10 | Requirement D1.1: In each round 1 of the log entries: #(entities generated) == #(overall entity count) ~ realInitialNumber
| 11 | Requirement D1.2: In all log entries: Current Darwin version is incremented with every simulation round.
| 12 | Requirement D1.3: In all log entries: percentageAccessedData * realInitialNumber * (dataGrowthRate + 1)^(#Round-1) ~ #(entities selected during workload), i.e. for all strategies holds that the deviation of the number of accessed entities remains within 5% of the specified input parameters, throughout all simulation rounds.
| 13 | Requirement D1.4: In all log entries: Workload: #(entities selected) == #(Player entities selected) + #(Mission entities selected) + #(Place entities selected), i.e. the sum of selected entities equals the sum of accessed entities of all types combined.
| 14 | Requirement D1.5: In all log entries: Migration Costs On-read: 'Migration cost == 0' for the Eager strategy.
| 15 | Requirement D1.6: In all log entries: #(Total migrated entities count) == Sum(#(entities eagerly/incrementally/proactively migrated)) + Sum(#(entities lazily migrated)), i.e. the total number of migrated entities of each round equals the sum of the migrated entities on-read and on-release.
| 16 | Requirement D1.8: In all log entries and for all types (Player/Mission/Place): overall up-to-date state: 100%; also x15 == 100%
| 17 | Requirement D1.9: In all log entries: #(overall entity count) =: x && for all types i: y of z_i entities are up-to-date => x == Sum(z_i), i.e. for all strategies the actuality rate of the entities is broken down for each type and for all simulation rounds.
| 18 | Requirement D1.11: In all log entries: #(overall entity count) ~ realInitialNumber * (dataGrowthRate + 1)^(#Round-1), i.e. for all strategies holds that the deviation of the number of entities remains within 5% of the specified input parameter of the real initial number plus the generated entities according to the data growth rate for each round, throughout all simulation rounds.
| 19 | Requirement D1.12: In all log entries: Round On-Read costs == 0 for all rounds of the Eager strategy, for every first round in general, and for all subsequent releases of the incremental rounds updating all entities.
| 20 | Requirement D1.13: In all log entries: Round On-Release costs + Round On-Read costs == Round Delta Cumulated costs.
| 21 | Requirement D1.14: In all log entries: Cumulated costs - Round Delta Cumulated costs == Cumulated costs of previous round
| 22 | Requirement D2.7: In all log entries: Round migration debt == 0 for all rounds of the Eager strategy.
| 23 | Requirement E2.7: In all log entries: Round migration debt == Sum(Player/Mission/Place debts) for all rounds of all strategies.
| 24 | Requirement E2.10: In all log entries: 's entities lazily migrated: Player x; Mission y; Place z;' => s == x + y + z, i.e. the sum of migrated entities on-read is broken down to the number of entities for each type.
| 25 | Requirement E2.11: In all log entries: Round On-Read costs > 0
| 26 | Requirement N1: For all input parameters and log entries holds: workloadExecutions == #(Workload) per round
| 27 | Requirement N2: For all input parameters and log entries holds: LET x + y + z == w && x == y / mission2playerCardinality && y == z / place2missionCardinality IN Workload: w entities selected: Player x; Mission y; Place z;
| 28 | Requirement N3: For all input parameters and log entries holds: schemaModifications == #(round) && for all migration strategy flags (e.g. eagerFlag) and for all instances of schemaModifications there exists an instance of a round
| 29 | Requirement N4: For all input parameters and log entries holds: IF complexity == 0 THEN operations element of {rename, add, delete} ELSE IF complexity == 100 THEN operations element of {copy, move} FI
Page updated
Google Sites
Report abuse