Tweeted twitter.com/StackCompSci/status/853664821623095297
5 edited tags
| link
4 formatting
source | link

Satisfying of $\square (\neg A U\cup B)$

Let's consider the following formula: $\square (\neg A U B)$$\square (\neg A \cup B)$.

Does the following computation satisfy it?

The numbers in brackets are number of state.

$(0) \neg A, \neg B \\ (1) \neg A, B \\ (2) A, \neg B $(0) $\neg A, \neg B$

(1) $\neg A, B$

(2) $A, \neg B$

$\square$ means that for every state in computation the formula $\neg A U B$$\neg A \cup B$ is satisfied, so: In $0$ state it is satisfied. In $1$ it is satfisfied. But, in $2$ state it is unsatisfied because $U$$\cup$ says that $A$ must be false until $B$ is true.

So, the formula is not satisfied.

But, it seems that my reasoning is incorrect because I test it for simple program in Promela and my tests suggest that the formula is satisified, though, my reasoning is incorrect.

Please help me .

inline test_and_set(addr, old) {
  d_step{
    old = addr;
    addr = 1;
  }
}
byte lock;
active [2] proctype proc(){
  byte old;
  do
  :: true ->
    wait:
      test_and_set(lock, old);
      do
      :: old != 0 -> test_and_set(lock, old);
      :: else -> break;
      od
    cs:
    lock = 0;
  od
}

ltl prop {((!proc[0]@cs) W proc[0]@wait) // (***)

And I verified it with spin -a test.pml ; gcc -O2 pan.c -o pan ; ./pan -a -f

And it has 0 errors. When I replace (***) with ltl prop{([](!proc[0]@cs) W proc[0]@wait))} I've got an error.

Why?

Satisfying of $\square (\neg A U B)$

Let's consider the following formula: $\square (\neg A U B)$.

Does the following computation satisfy it?

The numbers in brackets are number of state

$(0) \neg A, \neg B \\ (1) \neg A, B \\ (2) A, \neg B $

$\square$ means that for every state in computation the formula $\neg A U B$ is satisfied, so: In $0$ state it is satisfied. In $1$ it is satfisfied. But, in $2$ state it is unsatisfied because $U$ says that $A$ must be false until $B$ is true.

So, the formula is not satisfied.

But, it seems that my reasoning is incorrect because I test it for simple program in Promela and my tests suggest that the formula is satisified, though, my reasoning is incorrect.

Please help me .

inline test_and_set(addr, old) {
  d_step{
    old = addr;
    addr = 1;
  }
}
byte lock;
active [2] proctype proc(){
  byte old;
  do
  :: true ->
    wait:
      test_and_set(lock, old);
      do
      :: old != 0 -> test_and_set(lock, old);
      :: else -> break;
      od
    cs:
    lock = 0;
  od
}

ltl prop {((!proc[0]@cs) W proc[0]@wait) // (***)

And I verified it with spin -a test.pml ; gcc -O2 pan.c -o pan ; ./pan -a -f

And it has 0 errors. When I replace (***) with ltl prop{([](!proc[0]@cs) W proc[0]@wait))} I've got an error.

Why?

Satisfying of $\square (\neg A \cup B)$

Let's consider the following formula: $\square (\neg A \cup B)$.

Does the following computation satisfy it?

The numbers in brackets are number of state.

(0) $\neg A, \neg B$

(1) $\neg A, B$

(2) $A, \neg B$

$\square$ means that for every state in computation the formula $\neg A \cup B$ is satisfied, so: In $0$ state it is satisfied. In $1$ it is satfisfied. But, in $2$ state it is unsatisfied because $\cup$ says that $A$ must be false until $B$ is true.

So, the formula is not satisfied.

But, it seems that my reasoning is incorrect because I test it for simple program in Promela and my tests suggest that the formula is satisified, though, my reasoning is incorrect.

Please help me .

inline test_and_set(addr, old) {
  d_step{
    old = addr;
    addr = 1;
  }
}
byte lock;
active [2] proctype proc(){
  byte old;
  do
  :: true ->
    wait:
      test_and_set(lock, old);
      do
      :: old != 0 -> test_and_set(lock, old);
      :: else -> break;
      od
    cs:
    lock = 0;
  od
}

ltl prop {((!proc[0]@cs) W proc[0]@wait) // (***)

And I verified it with spin -a test.pml ; gcc -O2 pan.c -o pan ; ./pan -a -f

And it has 0 errors. When I replace (***) with ltl prop{([](!proc[0]@cs) W proc[0]@wait))} I've got an error.

Why?

3 added 682 characters in body
source | link

Let's consider the following formula: $\square (\neg A U B)$.

Does the following computation satisfy it?

The numbers in brackets are number of state

$(0) \neg A, \neg B \\ (1) \neg A, B \\ (2) A, \neg B $

$\square$ means that for every state in computation the formula $\neg A U B$ is satisfied, so: In $0$ state it is satisfied. In $1$ it is satfisfied. But, in $2$ state it is unsatisfied because $U$ says that $A$ must be false until $B$ is true.

So, the formula is not satisfied.

But, it seems that my reasoning is incorrect because I test it for simple program in Promela and my tests suggest that the formula is satisified, though, my reasoning is incorrect.

Please help me .

inline test_and_set(addr, old) {
  d_step{
    old = addr;
    addr = 1;
  }
}
byte lock;
active [2] proctype proc(){
  byte old;
  do
  :: true ->
    wait:
      test_and_set(lock, old);
      do
      :: old != 0 -> test_and_set(lock, old);
      :: else -> break;
      od
    cs:
    lock = 0;
  od
}

ltl prop {((!proc[0]@cs) W proc[0]@wait) // (***)

And I verified it with spin -a test.pml ; gcc -O2 pan.c -o pan ; ./pan -a -f

And it has 0 errors. When I replace (***) with `ltl prop{( W proc[0]@wait))}ltl prop{([](!proc[0]@cs) W proc[0]@wait))} I've got an error.

Why?

Let's consider the following formula: $\square (\neg A U B)$.

Does the following computation satisfy it?

The numbers in brackets are number of state

$(0) \neg A, \neg B \\ (1) \neg A, B \\ (2) A, \neg B $

$\square$ means that for every state in computation the formula $\neg A U B$ is satisfied, so: In $0$ state it is satisfied. In $1$ it is satfisfied. But, in $2$ state it is unsatisfied because $U$ says that $A$ must be false until $B$ is true.

So, the formula is not satisfied.

But, it seems that my reasoning is incorrect because I test it for simple program in Promela and my tests suggest that the formula is satisified, though, my reasoning is incorrect.

Please help me .

inline test_and_set(addr, old) {
  d_step{
    old = addr;
    addr = 1;
  }
}
byte lock;
active [2] proctype proc(){
  byte old;
  do
  :: true ->
    wait:
      test_and_set(lock, old);
      do
      :: old != 0 -> test_and_set(lock, old);
      :: else -> break;
      od
    cs:
    lock = 0;
  od
}

ltl prop {((!proc[0]@cs) W proc[0]@wait) // (***)

And I verified it with spin -a test.pml ; gcc -O2 pan.c -o pan ; ./pan -a -f

And it has 0 errors. When I replace (***) with `ltl prop{( W proc[0]@wait))} I've got an error.

Why?

Let's consider the following formula: $\square (\neg A U B)$.

Does the following computation satisfy it?

The numbers in brackets are number of state

$(0) \neg A, \neg B \\ (1) \neg A, B \\ (2) A, \neg B $

$\square$ means that for every state in computation the formula $\neg A U B$ is satisfied, so: In $0$ state it is satisfied. In $1$ it is satfisfied. But, in $2$ state it is unsatisfied because $U$ says that $A$ must be false until $B$ is true.

So, the formula is not satisfied.

But, it seems that my reasoning is incorrect because I test it for simple program in Promela and my tests suggest that the formula is satisified, though, my reasoning is incorrect.

Please help me .

inline test_and_set(addr, old) {
  d_step{
    old = addr;
    addr = 1;
  }
}
byte lock;
active [2] proctype proc(){
  byte old;
  do
  :: true ->
    wait:
      test_and_set(lock, old);
      do
      :: old != 0 -> test_and_set(lock, old);
      :: else -> break;
      od
    cs:
    lock = 0;
  od
}

ltl prop {((!proc[0]@cs) W proc[0]@wait) // (***)

And I verified it with spin -a test.pml ; gcc -O2 pan.c -o pan ; ./pan -a -f

And it has 0 errors. When I replace (***) with ltl prop{([](!proc[0]@cs) W proc[0]@wait))} I've got an error.

Why?

2 added 682 characters in body
source | link
1
source | link