LTL Properties
#	Machine	Property	Duration	Verified	Type	Description
1.	Win8	ltl solYes { ((environment.yes == 0 && environment.no == 0) || !isPsystemStep) U (environment.yes == 1 && environment.no == 0 && isPsystemStep) }	23'11''	TRUE	CMC13	This LTL property states that the number of yes and no objects in the environment is zero until a yes is sent to the environment
2.	Win8	ltl solNo { ((environment.yes == 0 && environment.no == 0) || !isPsystemStep) U (environment.yes == 0 && environment.no == 1 && isPsystemStep)}	16'57''	TRUE	CMC13	Is an LTL property stating that the number of yesand no objects in the environment is zero until a no is sent to the environement.
3.	Win8	ltl g1 {[] (!(c1Cells[0].a == 1 && c1Cells[0].T == 1) || X(!isPsystemStep U ((environment.yes==1) && isPsystemStep)) || !isPsystemStep) }	17'16''	TRUE	CMC13	LTL property stating that, if inside the mebrane labeled 1 there are present the a and T objects, then, in the next kP System state, an yes object will be sent to the environment.
4.	Win8	ltl g2 {[] (!(verifVarsFound && schedulerStep == verifStep &&  ((c2Cells[verifCellIndex].B[vtx1] >= 1 && c2Cells[verifCellIndex].B[vtx2] >= 1) ||  (c2Cells[verifCellIndex].G[vtx1] >= 1 && c2Cells[verifCellIndex].G[vtx2] >= 1) ||  (c2Cells[verifCellIndex].R[vtx1] >= 1 && c2Cells[verifCellIndex].R[vtx2] >= 1) )  && c2Cells[verifCellIndex].Aij[vtx1*N + vtx2] >= 1) ||  X(!isPsystemStep U (c2Cells[verifCellIndex].S == 0 && isPsystemStep)) || !isPsystemStep) }	24'32''	TRUE	CMC13 (invariant)	LTL property expressing that, if at the computation step given by verifStep, in a certain membrane labeled 2, given by the index verifCellIndex,  there exists an edge between (vtx1, vtx2), and the two verfices are both coloured in blue, green or red, then in the next kP System step, the S symbol from this membrane will disappear.
5.	Win8	ltl g3 {[] (!(schedulerStep >= N + 3) || (environment.yes==1 && isPsystemStep) || !isPsystemStep) }	39'32''	TRUE	IJCM-BWMC	This LTL property verifies that the answer to the question "is the graph G(N, k) 3-colourable" is "yes" and it is obtained after N + 3 kP System steps. The definition of G(N, k)is according to the one given in the IJCM - BWMC article.
6.	Win8	ltl g4 {[] (!(schedulerStep >= 2 * N + 3) || (Solutions == solCount && isPsystemStep) || !isPsystemStep) }	23'44''	TRUE	IJCM-BWMC	LTL property verifying that, when the computation stops, after at most 2 * N + 3 kP System steps, all the solCount =  3 * 2^(N - 1) valid solutions of the problem are obtained. This property holds for all the graphs G(N, k), as defined in the IJCM - BWMC article.
7.	Win8	ltl g5 {[] (!(schedulerStep <= N) || (totalActiveC2Cells == twoPowK && isPsystemStep) || !isPsystemStep) }	1h45'30	TRUE	IJCM-BWMC	This LTL property expresses that, for a graph of type G(N, N), as defined in the IJCM - BWMC article, the number of cells labeled 2 is 2^k after k steps, with  1 <= k <= N
8.	Win8	ltl g6 {[] (!(schedulerStep == N + 1) || (totalActiveC2Cells == twoPowK && isPsystemStep) || !isPsystemStep) }	1h55'48''	TRUE	IJCM-BWMC	LTL property verifying that, for a graph of type G(N, N), as defined in the IJCM - BWMC article, the number of cells labeled 2 is 2^(N + 1) - 1 at the N + 1 kP System step
9.	Win8	ltl g7 {[] (!(schedulerStep >= 2*N) || (totalActiveC2Cells == threePowK && isPsystemStep) || !isPsystemStep) }	2h4'59''	TRUE	IJCM-BWMC	LTL property verifying that, for a graph of type G(N, N), as defined in the IJCM - BWMC article, the number of cells labeled 2 is 3^N at the end of the division process, i.e. After 2^N kP System steps
10.	Win8	ltl g8 {[] (!(invariantPrecond) || X(!isPsystemStep U(invariantPostcond && isPsystemStep)) || !isPsystemStep) }	21'58''	TRUE	Invariant	LTL property of invariant type, verifying that, if invariantPrecond is true, i.e. there exists a compartemnt labeled 2 containing A_i and S at a certain step, then, at the next kP System step, invariantPostcond is true, i.e. there is a compartment containing R_i and S symbols, if and only if the graph has the neighbours of vertex i coloured different than red
Assertions
#	Machine	Property	Duration	Verified	Corresponding to LTL Property #
1.	Win 8	assert (invariantPrecond == false || schedulerStep != precondStep + 1 || invariantPostcond);	29'26''	VERDADERO	4.
Machine Configuration
Machine	Configuration
Win8	Intel Xeon X3430, 2.40 GHz, 8.0 GB RAM, Win8 64 bit