source: vis_dev/vis-2.3/models/counter/properties.ltl @ 86

Last change on this file since 86 was 28, checked in by cecile, 13 years ago

exemples de test
File size: 2.0 KB
Line 
1\define INIT (golden.bit0.value = 1 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (  faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (  faulty.bit1.value = 0 * (  faulty.bit2.value = 0)))))+ golden.bit0.value = 0 * (golden.bit1.value = 1 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 )))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0))))+ golden.bit1.value = 0 * (golden.bit2.value = 1 * (faulty.bit0.value = 1 * (  faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (faulty.bit2.value = 1 )+ faulty.bit1.value = 0 * (  faulty.bit2.value = 0)))+ golden.bit2.value = 0 * (faulty.bit0.value = 1 * (  faulty.bit1.value = 0 * (  faulty.bit2.value = 0))+ faulty.bit0.value = 0 * (faulty.bit1.value = 1 * (  faulty.bit2.value = 0)+ faulty.bit1.value = 0 * (faulty.bit2.value = 1 ))))))
Note: See TracBrowser for help on using the repository browser.