From: Kish Shen <kisshen_at_cisco.com>

Date: Fri, 11 Apr 2008 23:04:28 +0100

Date: Fri, 11 Apr 2008 23:04:28 +0100

Valerio wrote: > No, the tool itself is written in C++. > Normally, it would ne much easier to write something like this in ECLiPSe itself. Was there any specific reasons why C++ was used? In addition, if you could generate the constraints in a printed form, to be placed into a file, you should be able to generate the constraint in a form that you can post directly, as Joachim suggested. I am not sure if you are familiar with ECLiPSe/Prolog, but constraints (and expressions in general) are just Prolog structures, so you should be able to build any expression when you run a ECLiPSe program, i.e. a constraint does not have to appear in source form (this is unlike expressions in languages such as C, for example). For example, you can have a rule: negate(E, NegatedE) :- NegatedE = neg(E). which creates a negated version of E. So you should be able to write rules to build the subexpressions for and, or, etc, as you have shown in your example. and when you created your final expression, you should be able to just post it: ... generate_one_constraint(Data, Constraint), ic:Constraint, where Data is the data you need to generate the constraint (you can of course read this in from a data file). Cheers, Kish . > 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 Guarnieri > > ------------------------------------------------------------------------- > This SF.net email is sponsored by the 2008 JavaOne(SM) Conference > Don't miss this year's exciting event. There's still time to save $100. > Use priority code J8TL2D2. > http://ad.doubleclick.net/clk;198757673;13503038;p?http://java.sun.com/javaone > _______________________________________________ > ECLiPSe-CLP-Users mailing list > ECLiPSe-CLP-Users_at_lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/eclipse-clp-users >Received on Fri Apr 11 2008 - 15:04:38 CEST

*
This archive was generated by hypermail 2.2.0
: Thu Feb 02 2012 - 02:31:58 CET
*