[sv-ac] #1502 (Property evaluation attempts and decision points) (correction)

Hi all,

 

I realized that my definition of the failure points of a sequence is
wrong - has the same problem as pointed below. Will add an inductive
definition next week.

 

Thanks,

Dmitry

 

 

Following our last meeting minutes I am submitting a Mantis item
containing a formal definition of an assertion attempt failure and
success (=decision) points. I am giving an inductive definition which is
rather sophisticated. A simple definition as 

 

Let $A = \{j| w^{0,j-1}\bot^\omega \models P\}$. $i$ is a property
success point iff $A \ne \emptyset$ and $i = \min{A}$.

Let $B = \{j| w^{0,j-1}\top^\omega \nvDash P\}$. $i$ is a property
failure point iff $B \ne \emptyset$ and $i = \min{B}$.

 

does not  look good, since in such a case we would have to report the
failure of the following property

 

1 |-> ((##1000 a) and (##1000 !a)) 

 

at the initial cycle. Most tools won't detect the failure before the
1000th cycle, however.

 

Any formal definition of a decision point has the drawback that it
forbids any optimizations during simulation. On the other hand, it looks
strange if there is no exact definition of the time when the action
block should be executed. I am also concerned about integrating an
automata-oriented simulation approach with this definition.

 

Thanks,

Dmitry