I have two following statements in the model (the program model is the self-composed model of a program with parallel composition):
c_code{};
(!lock);
The first statement is always followed by the second one. So, I wrapped these two statements as an atomic sequence as follows:
atomic{
c_code{};
(!lock);
}
As expected, the number of states were decreased for concurrent programs (when lock is zero, the sequence is executed indivisibly).
But, the result for sequential programs was surprising, where the number of states were increased a bit little! I cannot understand why?!
many thanks in advance
]]>