No, the tool itself is written in C++. Here is the complete for code for a small example. I omitted the faulty version of the EFSM, as it would be pretty redundant in this case: % main for loop (for(I,1,T1), param( IN1, IN2, OUT1, OUT2, REG, A, B, C, A_F, B_F, C_F, OUT1_F, OUT2_F, REG_F, E1, E2, E3, E4, E5, E6, E7, E1_F, E2_F, E3_F, E4_F, E5_F, E6_F, E7_F ) do ( I1 is I+1, % constraint on signals and states at each clock cycle neg((REG[I] #= REG_F[I]) and (A[I] #= A_F[I]) and (B[I] #= B_F[I]) and (C[I] #= C_F[I])), % ----- FAULT FREE ----- % constraint on state activity in each clock cycle ((A[I] and neg(B[I]) and neg(C[I])) or (B[I] and neg(A[I]) and neg(C[I])) or (C[I] and neg(A[I]) and neg(B[I]))), % constraint on transition activity in each clock cycle ((E1[I] and neg(E2[I]) and neg(E3[I]) and neg(E4[I]) and neg(E5[I]) and neg(E6[I]) and neg(E7[I])) or (E2[I] and neg(E1[I]) and neg(E3[I]) and neg(E4[I]) and neg(E5[I]) and neg(E6[I]) and neg(E7[I])) or (E3[I] and neg(E1[I]) and neg(E2[I]) and neg(E4[I]) and neg(E5[I]) and neg(E6[I]) and neg(E7[I])) or (E4[I] and neg(E1[I]) and neg(E2[I]) and neg(E3[I]) and neg(E5[I]) and neg(E6[I]) and neg(E7[I])) or (E5[I] and neg(E1[I]) and neg(E2[I]) and neg(E3[I]) and neg(E4[I]) and neg(E6[I]) and neg(E7[I])) or (E6[I] and neg(E1[I]) and neg(E2[I]) and neg(E3[I]) and neg(E4[I]) and neg(E5[I]) and neg(E7[I])) or (E7[I] and neg(E1[I]) and neg(E2[I]) and neg(E3[I]) and neg(E4[I]) and neg(E5[I]) and neg(E6[I]))), % transition #1 (C[I] and neg(IN2[I] #= 0)) => E1[I], E1[I] => (C[I] and neg(IN2[I] #= 0)), (E1[I] and ((C[I] and neg(IN2[I] #= 0)))) => (REG[I1] #= REG[I] + IN2[I] and OUT1[I1] #= 1 and OUT2[I1] #= 1), % transition #2 (C[I] and neg(neg(IN2[I] #= 0)) and IN1[I] #= 0) => E2[I], E2[I] => (C[I] and neg(neg(IN2[I] #= 0)) and IN1[I] #= 0), (E2[I] and ((C[I] and neg(neg(IN2[I] #= 0)) and IN1[I] #= 0))) => (OUT1[I1] #= REG[I] and OUT2[I1] #= quot_div(REG[I],2) and REG[I1] #= REG[I]), % transition #3 (C[I] and neg(neg(IN2[I] #= 0)) and neg(IN1[I] #= 0)) => E3[I], E3[I] => (C[I] and neg(neg(IN2[I] #= 0)) and neg(IN1[I] #= 0)), (E3[I] and ((C[I] and neg(neg(IN2[I] #= 0)) and neg(IN1[I] #= 0)))) => (OUT1[I1] #= quot_div(REG[I],2) and OUT2[I1] #= REG[I] and REG[I1] #= REG[I]), % transition #4 (A[I] and neg(neg(IN1[I] #= 0))) => E4[I], E4[I] => (A[I] and neg(neg(IN1[I] #= 0))), (E4[I] and ((A[I] and neg(neg(IN1[I] #= 0))))) => (REG[I1] #= IN2[I] and OUT1[I1] #= 0 and OUT2[I1] #= 0), % transition #5 (A[I] and neg(IN1[I] #= 0)) => E5[I], E5[I] => (A[I] and neg(IN1[I] #= 0)), (E5[I] and ((A[I] and neg(IN1[I] #= 0)))) => (REG[I1] #= IN1[I] and OUT1[I1] #= 1 and OUT2[I1] #= 1), % transition #6 (B[I] and neg(REG[I] #= 1)) => E6[I], E6[I] => (B[I] and neg(REG[I] #= 1)), (E6[I] and ((B[I] and neg(REG[I] #= 1)))) => (OUT1[I1] #= 0 and OUT2[I1] #= 0 and REG[I1] #= REG[I]), % transition #7 (B[I] and neg(neg(REG[I] #= 1))) => E7[I], E7[I] => (B[I] and neg(neg(REG[I] #= 1))), (E7[I] and ((B[I] and neg(neg(REG[I] #= 1))))) => (OUT1[I1] #= REG[I] * 2 and OUT2[I1] #= REG[I] and REG[I1] #= REG[I]), % constraint for state A A[I1] #= ((E1[I] and (neg(E2[I])) and (neg(E3[I])) and (neg(E6[I]))) or (E2[I] and (neg(E1[I])) and (neg(E3[I])) and (neg(E6[I]))) or (E3[I] and (neg(E1[I])) and (neg(E2[I])) and (neg(E6[I]))) or (E6[I] and (neg(E1[I])) and (neg(E2[I])) and (neg(E3[I])))), % constraint for state B B[I1] #= ((E5[I] and (neg(E7[I]))) or (E7[I] and (neg(E5[I])))), % constraint for state C C[I1] #= ((E4[I])), % implication for state A (E1[I] or E2[I] or E3[I] or E6[I]) => A[I1], % implication for state B (E5[I] or E7[I]) => B[I1], % implication for state C (E4[I]) => C[I1], % end of the main for loop )), In the meanwhile, I thought of a possible solution to the arguments limit. Probably I should use just one variable for each transition (e.g. a variable named E) and make it an array with as many elements as the number of transitions. For example, instead of writing E5 I might write E[5]. Do you think such a solution would be feasible? Valerio GuarnieriReceived on Fri Apr 11 2008 - 09:54:32 CEST
This archive was generated by hypermail 2.2.0 : Thu Feb 02 2012 - 02:31:58 CET