| 2015-04-15 14:53:22 |
Danil Sokolov |
bug |
|
|
added bug |
| 2015-04-15 14:53:22 |
Danil Sokolov |
attachment added |
|
stg-vme-read_write.work https://bugs.launchpad.net/bugs/1444513/+attachment/4376283/+files/stg-vme-read_write.work |
|
| 2015-04-15 14:55:06 |
Danil Sokolov |
description |
Normalcy checking can have 3 types of outputs for the case of violation. |
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. |
|
| 2015-04-15 15:04:14 |
Danil Sokolov |
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. |
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. Examples of the output to follow. |
|
| 2015-04-15 15:17:30 |
Danil Sokolov |
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. Examples of the output to follow. |
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_Normalcy::print_results(ostream& os) const{
switch(normalcy_violation_reason){
case nvr_mixed_triggers:
ASSERT(paths.size()==1);
print_sequence(paths[0],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set1,os);
ASSERT(!signal_name.empty());
os<<"\nNormalcy violation due to different triggers' signs for signal "<<signal_name<<'\n';
}
break;
case nvr_contradictious_hypotheses:
ASSERT(paths.size()==2);
print_sequence(paths[0],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set1,os);
}
print_sequence(paths[1],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set2,os);
os<<
"\nNormalcy violation due to contradictious normalcy type hypotheses for signal "<<
signal_name<<
"\n(the paths show violations of p- and n-normalcy correspondingly)\n";
}
break;
case nvr_CSC_conflict:
print_sequence(paths[0],os);
print_sequence(paths[1],os);
os<<"\nNormalcy violation due to a CSC conflict for signal "<<signal_name<<'\n';
break;
case nvr_other:
print_sequence(paths[0],os);
os<<"triggers: ";
print_sequence(trig_set1,os);
print_sequence(paths[1],cout);
print_sequence(paths[2],cout);
ASSERT(n_type!=0);
cout<<
"\nNormalcy violation for signal "<<signal_name<<':'<<
'\n'<<(n_type==STG_TS_PLUS ? 'p' : 'n')<<"-normalcy is violated according to the first path"<<
'\n'<<(n_type==STG_TS_PLUS ? 'n' : 'p')<<"-normalcy is violated according to the other two paths\n";
break;
case nvr_no_violation:
default:
ASSERT0;
}
} |
|
| 2015-04-15 15:18:16 |
Danil Sokolov |
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_Normalcy::print_results(ostream& os) const{
switch(normalcy_violation_reason){
case nvr_mixed_triggers:
ASSERT(paths.size()==1);
print_sequence(paths[0],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set1,os);
ASSERT(!signal_name.empty());
os<<"\nNormalcy violation due to different triggers' signs for signal "<<signal_name<<'\n';
}
break;
case nvr_contradictious_hypotheses:
ASSERT(paths.size()==2);
print_sequence(paths[0],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set1,os);
}
print_sequence(paths[1],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set2,os);
os<<
"\nNormalcy violation due to contradictious normalcy type hypotheses for signal "<<
signal_name<<
"\n(the paths show violations of p- and n-normalcy correspondingly)\n";
}
break;
case nvr_CSC_conflict:
print_sequence(paths[0],os);
print_sequence(paths[1],os);
os<<"\nNormalcy violation due to a CSC conflict for signal "<<signal_name<<'\n';
break;
case nvr_other:
print_sequence(paths[0],os);
os<<"triggers: ";
print_sequence(trig_set1,os);
print_sequence(paths[1],cout);
print_sequence(paths[2],cout);
ASSERT(n_type!=0);
cout<<
"\nNormalcy violation for signal "<<signal_name<<':'<<
'\n'<<(n_type==STG_TS_PLUS ? 'p' : 'n')<<"-normalcy is violated according to the first path"<<
'\n'<<(n_type==STG_TS_PLUS ? 'n' : 'p')<<"-normalcy is violated according to the other two paths\n";
break;
case nvr_no_violation:
default:
ASSERT0;
}
} |
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_Normalcy::print_results(ostream& os) const{
switch(normalcy_violation_reason){
case nvr_mixed_triggers:
ASSERT(paths.size()==1);
print_sequence(paths[0],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set1,os);
ASSERT(!signal_name.empty());
os<<"\nNormalcy violation due to different triggers' signs for signal "<<signal_name<<'\n';
}
break;
case nvr_contradictious_hypotheses:
ASSERT(paths.size()==2);
print_sequence(paths[0],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set1,os);
}
print_sequence(paths[1],os);
if(&os==&cout){
os<<"triggers: ";
print_sequence(trig_set2,os);
os<<
"\nNormalcy violation due to contradictious normalcy type hypotheses for signal "<<
signal_name<<
"\n(the paths show violations of p- and n-normalcy correspondingly)\n";
}
break;
case nvr_CSC_conflict:
print_sequence(paths[0],os);
print_sequence(paths[1],os);
os<<"\nNormalcy violation due to a CSC conflict for signal "<<signal_name<<'\n';
break;
case nvr_other:
print_sequence(paths[0],os);
os<<"triggers: ";
print_sequence(trig_set1,os);
print_sequence(paths[1],cout);
print_sequence(paths[2],cout);
ASSERT(n_type!=0);
cout<<
"\nNormalcy violation for signal "<<signal_name<<':'<<
'\n'<<(n_type==STG_TS_PLUS ? 'p' : 'n')<<"-normalcy is violated according to the first path"<<
'\n'<<(n_type==STG_TS_PLUS ? 'n' : 'p')<<"-normalcy is violated according to the other two paths\n";
break;
case nvr_no_violation:
default:
ASSERT0;
}
}
Currently normalcy violation is correctly checked for a single trace only (case nvr_mixed_triggers). |
|
| 2015-04-15 15:28:29 |
Launchpad Janitor |
branch linked |
|
lp:~danilovesky/workcraft/trunk-bug-1444513 |
|
| 2015-04-17 14:58:27 |
Danil Sokolov |
workcraft: status |
Confirmed |
In Progress |
|
| 2015-04-17 14:58:59 |
Danil Sokolov |
workcraft: status |
In Progress |
Confirmed |
|
| 2015-04-23 12:23:40 |
Launchpad Janitor |
branch linked |
|
lp:workcraft |
|
