5 edited tags
4 formatting

# 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.

inline test_and_set(addr, old) {
d_step{
}
}
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.

inline test_and_set(addr, old) {
d_step{
}
}
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.

inline test_and_set(addr, old) {
d_step{
}
}
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

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.

inline test_and_set(addr, old) {
d_step{
}
}
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.

inline test_and_set(addr, old) {
d_step{
}
}
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.

inline test_and_set(addr, old) {
d_step{
}
}
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
1