Checking of STG normalcy has an error
Affects | Status | Importance | Assigned to | Milestone | |
---|---|---|---|---|---|
Workcraft |
Confirmed
|
Low
|
Danil Sokolov |
Bug Description
Normalcy checking returns "property" satisfied for the attached example, even though there is a violation. This is due to incorrect parsing of the MPSat output.
Normalcy checking can have 3 types of outputs for the case of violation that need to be considered. Victor could not find a benchmark for the complicated case. Below is the printing code - 1, 2 or 3 traces are printed depending on the circumstances.
void solution_
switch(
case nvr_mixed_triggers:
ASSERT(
print_
if(&os==&cout){
os<<"triggers: ";
print_
ASSERT(
os<<"\nNormalcy violation due to different triggers' signs for signal "<<signal_
}
break;
case nvr_contradicti
ASSERT(
print_
if(&os==&cout){
os<<"triggers: ";
print_
}
print_
if(&os==&cout){
os<<"triggers: ";
print_
os<<
"\nNormalcy violation due to contradictious normalcy type hypotheses for signal "<<
signal_name<<
"\n(the paths show violations of p- and n-normalcy correspondingly
}
break;
case nvr_CSC_conflict:
print_
print_
os<<"\nNormalcy violation due to a CSC conflict for signal "<<signal_
break;
case nvr_other:
print_
os<<"triggers: ";
print_
print_
print_
ASSERT(
cout<<
"\nNormalcy violation for signal "<<signal_
'\n'
'\n'
break;
case nvr_no_violation:
default:
ASSERT0;
}
}
Currently normalcy violation is correctly checked for a single trace only (case nvr_mixed_
description: | updated |
description: | updated |
Changed in workcraft: | |
status: | Confirmed → In Progress |
status: | In Progress → Confirmed |
Currently normalcy violation is correctly checked for a single trace.