How to analysis untested DCPs from TTM model

[jack]

In TTM model ,the condition as below:

NOT ((AInput > 3
AND AInput < 5
AND BInput > 6)
OR (AInput <= 3
OR AInput >= 5
AND BInput <= 6))

In this case,TVGS report some untested DCPs.I know these untested DCPs not means there are some problem in TTM model.

But,I want to know how can I know if there is any problem in TTM model when there are so many untested
DCPs,maybe some just like this example,some means there are problem in TTM model.

Must I analysis these untest DPCs one by one? Sometimes,I find there are some many untested
DCPs like this example.

[busser]

TTM is a requirements modeling tool. This means that every relationship that is expressed in TTM is "required". If a user creates a condition table that states

if (A && (B || C)) then table_output = 1

this means precisely that the requirements are

if (A && B) then table_output = 1
if (A && C) then table_output = 1

each of these 2 disjunctive expressions are individual requirements. T-VEC will generate tests to verify each of these requirements.

If, however, the user creates a condition table that states

if (A && (B || !A)) then table_output = 1

this means that the requirements are

if (A && B) then table_output = 1
if (A && !A) then table_output = 1

T-VEC will again try to produce tests for each "requirement". The second "if" case will obviously fail because it is not possible for (A && !A). However, this is what the user specified. T-VEC can not decide if it is ok to the user to ignore this case. T-VEC can only indicate the contradiction, it is up to the user to determine if it is acceptable in the TTM model or not.

In TTM, all test vector failures mean there is something wrong with the model. However, in some cases users prefer the simplicity of writing expressions like this

NOT ((AInput > 3
AND AInput < 5
AND BInput > 6)
OR (AInput <= 3
OR AInput >= 5
AND BInput <= 6))

rather than to re-write the expression in a way that removes any contradictory cases. This often happens when users take a expression like

((AInput > 3
AND AInput < 5
AND BInput > 6)
OR (AInput <= 3
OR AInput >= 5
AND BInput <= 6))

which specifies a set of condition disjunctions that are all valid requirements, and then they try to specify the opposite case by placing a NOT() around the first expression. For example

not_case.png (48.87 KiB) Viewed 1144 times

Users often don't fully realize the meaning of NOT(<expr>). Placing NOT() around an expression, and than factoring that expression into disjunctive normal form logic (DCP's), in order to identify all possible ways that the total expression can evaluate to TRUE, requires that DeMorgan's Law be applied to the expression.

DeMorgan's Law : NOT(A || B) == NOT(A) && NOT(B)
NOT(A && B) == NOT(A) || NOT(B)

The vector generation errors you are seeing in your model are true errors in the model. They are cases where the logic states conditions that are "required". In some of these cases, the requirements are not realizable.

If such errors are not desired, the user should write only the valid/realizable requirements into the TTM tables. The first step to determining which are the valid/realizable requirements from expressions such as

NOT ((AInput > 3
AND AInput < 5
AND BInput > 6)
OR (AInput <= 3
OR AInput >= 5
AND BInput <= 6))

would be to convert the expression to disjunctive normal form. The first 4 steps are just to distribute the NOT operator.

Step 1:
NOT((AInput > 3) AND (AInput < 5) AND (BInput > 6))
AND
NOT((AInput <= 3) OR ((AInput >= 5) AND (BInput <= 6)))

Step 2:
(NOT(AInput > 3) OR NOT(AInput < 5) OR NOT(BInput > 6))
AND
(NOT(AInput <= 3) AND NOT((AInput >= 5) AND (BInput <= 6)))

Step 3:
(NOT(AInput > 3) OR NOT(AInput < 5) OR NOT(BInput > 6))
AND
(NOT(AInput <= 3) AND (NOT(AInput >= 5) OR NOT(BInput <= 6)))

Step 4:
(NOT(AInput > 3) OR NOT(AInput < 5) OR NOT(BInput > 6))
AND
NOT(AInput <= 3)
AND
(NOT(AInput >= 5) OR NOT(BInput <= 6))

Step 5: convert to disjunctive normal form clauses

DCP 1 : NOT(AInput > 3) AND NOT(AInput <= 3) AND NOT(AInput >= 5)
DCP 2 : NOT(AInput > 3) AND NOT(AInput <= 3) AND NOT(BInput <= 6)
DCP 3 : NOT(AInput < 5) AND NOT(AInput <= 3) AND NOT(AInput >= 5)
DCP 4 : NOT(AInput < 5) AND NOT(AInput <= 3) AND NOT(BInput <= 6)
DCP 5 : NOT(BInput > 6) AND NOT(AInput <= 3) AND NOT(AInput >= 5)
DCP 6 : NOT(BInput > 6) AND NOT(AInput <= 3) AND NOT(BInput <= 6)

Each of these DCP's are directly implied to be "requirements" by the statement in TTM in row 2

not_case.png (48.87 KiB) Viewed 1144 times

However, it should be easy to recognize (at least in this case) that DCPs 1,2,3,6 are all unrealizable - they contain inherent contradictions - such as NOT(AInput > 3) AND NOT(AInput <= 3). So, if the desire is to specify in the model, only truly realizable requirements (rather than take the easy way of NOT'ing an existing fully realizable expression) one could specify the requirements like this

realizable.png (4.98 KiB) Viewed 1140 times

I would like to point out, however, that it is not necessary to do these logical reductions by hand. The TTM translator performs the DeMorganization steps necessary to break a NOT'ed expression into its individual DCP's. Then the T-VEC compiler can identify tautological contradictions, such as the ones in this example, and it displays this information in the DCP view (making the DCP icon red) and in the tautological contradiction report.

dcp_view.png (87.99 KiB) Viewed 1137 times

If the DCP expression is not realizable, but also not directly identifiable as being contradictory by the T-VEC compiler, the user can review the vector generation failures that result and then modify the TTM model accordingly.