Deriving Filtering Algorithms from Constraint Checkers
Nicolas Beldiceanu,Mats Carlsson,and Thierry Petit LINA FRE CNRS2729,′Ecole des Mines de Nantes,FR-44307Nantes Cedex3,France.
Nicolas.Beldiceanu,Thierry.Petit@emn.fr
SICS,P.O.Box1263,SE-16429Kista,Sweden.
Mats.Carlsson@sics.se
April27,2004
SICS Technical Report T2004:08
ISRN:SICS-T–2004/08-SE
ISSN:1100-3154
Abstract.This reportdeals with global constraints for which the set of solutions
can be recognized by an extended?nite automaton whose size is bounded by
a polynomial in,where is the number of variables of the corresponding
global constraint.By reformulating the automaton as a conjunction of signature
and transition constraints we show how to systematically obtain a?ltering al-
gorithm.Under some restrictions on the signature and transition constraints this
?ltering algorithm achieves arc-consistency.An implementation based on some
constraints as well as on the metaprogramming facilities of SICStus Prolog is
available.For a restricted class of automata we provide a?ltering algorithm for
the relaxed case,where the violation cost is the minimum number of variables to
unassign in order to get back to a solution.Keywords:Constraint Programming,
Global Constraints,Filtering Algorithms,Finite Automata,Relaxation.
1Introduction
Deriving?ltering algorithms for global constraints is usually far from obvious and re-quires a lot of energy.As a?rst step toward a methodology for semi-automatic de-velopment of?ltering algorithms for global constraints,Carlsson and Beldiceanu have introduced[12]an approach to design?ltering algorithms by derivation from a?nite automaton.As quoted in their discussion,constructing the automaton was far from obvi-ous since it was mainly done as a rational reconstruction of an emerging understanding of the necessary case analysis related to the required pruning.However,it is commonly admitted that coming up with a checker which tests whether a ground instance is a solution or not is usually straightforward.This was for instance done for constraints de-?ned in extension?rst by Vempaty[29]and later on by Amilhastre et al.[2].This was also done for arithmetic constraints by Boigelot and Wolper[10].Within the context of global constraints on a?nite sequence of variables,the recent work of Pesant[26] uses also a?nite automaton for constructing a?ltering algorithm.This reportfocuses on
those global constraints that can be checked by scanning once through their variables without using any extra data structure.
As a second step toward a methodology for semi-automatic development of?ltering algorithms,we introduce a new approach which only requires de?ning a?nite automa-ton that checks a ground instance.We extend traditional?nite automata in order not to be limited only to regular expressions.Our?rst contribution is to show how to reformu-late the automaton associated with a global constraint as a conjunction of signature and transition constraints.We characterize some restrictions on the signature and transition constraints under which the?ltering algorithm induced by this reformulation achieves arc-consistency and apply this new methodology to the three following problems:
–The design of?ltering algorithms for a fairly large set of global constraints.
–The design of?ltering algorithms for handling the conjunction of several global constraints.
–The design of constraints for dealing with problems involving?nite state systems where the transition diagram is known.
Our second contribution is to provide for a restricted class of automata a?ltering algorithm for the relaxed case.This technique relies on the variable based violation cost introduced in[27,24].This cost was advocated as a generic way for expressing the violation of a global constraint.However,algorithms were only provided for the soft
con-
2
tiguity[23],lexicographic ordering[18],among[6]and inflexion[3]. Since they illustrate key points needed for characterizing the set of solutions associated with a global constraint,our discussion will be based on the last four constraints for which we now recall the de?nition:
–The global
contiguity holds since we have only one group of consecutive1.
–The lexicographic ordering constraint over two vectors of variables
and holds iff or or and.
–The among constraint restricts the number of variables of the sequence of variables,which take their value in a given set,to be equal to the variable.For instance,among holds since ex-actly3values of the sequence are located in.
–The inflexion constraint enforces the number of in?exions of the sequence of variables to be equal to the variable.An inflexion is described by one of the following patterns:a strict increase followed by a strict decrease or,conversely,a strict decrease followed by a strict increase.For instance, inflexion holds since we can extract from the sequence the four subsequences,,and,which all follow one of these two patterns.
Parts(A1),(B1),(C1)and(D1)of Fig.1depict the four checkers respectively associated with global
contiguity constraint,some transitions now correspond to a condi-tion(e.g.,)between two variables of the constraint.
–Observe that the among constraint involves a variable
whose value is computed from a given collection of variables.The checker de-picted by part(C1)of Fig.1counts the number of variables of
3
$ $ vars[i] notin values x[i]=y[i]vars[i]in values,c++ t nvar=c t: c=0 s: s 1 BEGIN 2 i=0; 3 WHILE i 4 WHILE i 5 WHILE i 6 RETURN (i=n); 7 END. global_contiguity (vars[0..n?1]):BOOLEAN among 1 BEGIN 2 i=0; 3 WHILE i 4 RETURN (i=n OR x[i] 5 END. among 1 BEGIN 2 i=0; c=0; 3 WHILE i 4 IF vars[i] in values THEN c++;6 RETURN (nvar=c); 5 i++; 7 END. inflexion 01 BEGIN 02 i=0; c=0; 03 WHILE i 04 IF i 05 WHILE i 06 IF less THEN 07 IF vars[i]>vars[i+1] THEN c++; less:=FALSE;08 ELSE 09 IF vars[i] 11 RETURN (ninf=c);12 END. (nvar,vars[0..n?1],values):BOOLEAN (ninf,vars[0..n?1]):BOOLEAN vars[i]=0vars[i]=1vars[i]=0 vars[i]=0 $ $vars[i]=1$ t z n s global_contiguity i j $vars[i+1] vars[i]=$vars[i]=vars[i+1] vars[i] vars[i] vars[i]= vars[i+1] $vars[i+1]vars[i]>vars[i+1] vars[i]> ninf=c t:c=0 s: inflexion c++ vars[i]>vars[i+1],vars[i] (B1) (C1) (D1)(A2)(B2) (C2) (D2) (x[0..n?1],y[0..n?1]):BOOLEAN Fig.1.Four checkers and their corresponding automata. 4 that take their value in.For this purpose it uses a counter,which is even-tually tested against the value of.This convinced us to allow the use of coun-ters in an automaton.Each counter has an initial value which can be updated while triggering certain transitions.The?nal state of an automaton can enforce a variable of the constraint to be equal to a given counter.Part(C2)of Fig.1describes the automaton corresponding to the code given in part(C1)of the same?gure.The au-tomaton uses the counter variable initially set to and takes as input the sequence .It triggers a transition for each variable of this sequence and increments when the corresponding variable takes its value in.The ?nal state returns a success when the value of is equal to.At this point we want to stress the following fact:It would have been possible to use an automaton which avoids the use of counters.However,this automaton would depend on the effective value of the parameter.In addition,it would require more states than the automaton of part(C2)of Fig.1.This is typically a problem if we want to have a?xed number of states in order to save memory as well as time. –As the among constraint,the inflexion constraint involves a variable whose value is computed from a given sequence of variables .Therefore,the checker depicted in part(D1)of Fig.1 uses also a counter for counting the number of in?exions,and compares its?nal value to the parameter.This program is represented by the automaton depicted by part(D2)of Fig.1.It takes as input the sequence of pairs and triggers a transition for each pair.Observe that a given variable may occur in more than one pair.Each transition compares the respective values of two consecutive variables of and increments the counter when a new in?exion is detected.The?nal state returns a success when the value of is equal to. Synthesizing all the observations we got from these examples leads to the following remarks and de?nitions for a given global constraint: –For a given state,no transition can be triggered indicates that the constraint does not hold. –Since all transitions starting from a given state are mutually incompatible all au-tomata are deterministic.Let denote the set of mutually incompatible conditions associated with the different transitions of an automaton. –Let denote the sequence of subsets of variables of on which the transitions are successively triggered.All these subsets contain the same number of elements and refer to some variables of.Since these subsets typically depend on the constraint,we leave the computation of outside the automaton. To each subset of this sequence corresponds a variable with an initial domain ranging over,where is a?xed integer.To each integer of this range corresponds one of the mutually incompatible conditions of.The sequences and are respectively called the signature and the signature argument of the constraint.The constraint between and the variables of is called the signature constraint and is denoted by. –From a pragmatic point the view,the task of writing a constraint checker is naturally done by writing down an imperative program where local variables,assignment 5 statements and control structures are used.This suggested us to consider determin-istic?nite automata augmented with local variables and assignment statements on these variables.Regarding control structures,we did not introduce any extra feature since the deterministic choice of which transition to trigger next seemed to be good enough. –Many global constraints involve a variable whose value is computed from a given collection of variables.This convinced us to allow the?nal state of an automaton to optionally return a result.In practice,this result corresponds to the value of a local variable of the automaton in the?nal state. De?ning an Automaton.An automaton of a constraint is de?ned by a septuple ,,,, ,, where: –is the sequence of variables corresponding to the signa-ture of the constraint. –is an interval which de?nes the range of possible values of the variables of. –is the signature argument of the constraint.The link between the variables of and the variable is done by writing down the signature constraint in such a way that arc-consistency is achieved.In our context this is done by using standard features of the CLP(FD) solver of SICStus Prolog[13]such as arithmetic constraints between two variables, propositional combinators or the global constraints programming interface. –When used,de?nes a symbolic name for each term of .These names can be used within the description of a transition for expressing an additional condition for triggering the corresponding transition. –is the,possibly empty,list of all counters used in the automaton.Each counter is described by a term where is a symbolic name representing the counter,is an integer giving the value of the counter in the initial state of,and gives the variable that should be uni?ed with the value of the counter in the?nal state of.–is the list of states of,where each state has the form, or.is a unique identi?er associated with each state.Finally, and respectively denote the initial and the?nal state of. –is the list of transitions of.Each transition has the form or.and respectively cor-respond to the state just before and just after,while depicts the value that the signature variable should have in order to trigger.When used,gives for each counter of its value after?ring the corresponding transition.This value is speci?ed by an arithmetic expression involving counters,constants,as well as usual arithmetic functions such as,,or.The order used in the list is identical to the order used in. 6 Example1.As an illustrative example we give the description of the automaton associated with the inflexion constraint.We have: –, –, –=, –is not used, –, –, – . The signature constraint relating each pair of variables to the signature variable is de?ned as follows:inflexion .The sequence of transitions triggered on the ground instance inflexion,is .Each transition gives the corresponding condition and,eventually,the value of the counter just after?ring that transition. 3Filtering Algorithm The?ltering algorithm is based on the following idea.For a given global constraint, one can think of its automaton as a procedure that repeatedly maps a current state and counter vector,given a signature variable,to a new state and counter vector ,until a terminal state is reached.We then convert this procedure into a transition constraint as follows.Assuming that the automaton asso-ciated with has arcs,the transition constraint has the following form,implemented with arithmetic,case1,and element constraints[13]: . . . We can then arrive at a?ltering algorithm for by decomposing it into a conjunction of constraints,“threading”the state and counter variables through the conjunction. In addition to this,we need the signature constraints that relate each signature variables to the variables of its corresponding signature argument .Filtering for the constraint is provided by the conjunction of all signature and transitions constraints,(being the start state and being the end state): . . . (A)(B) Fig.2.Automata and decision trees for(A)and(B)among. A couple of examples will help clarify this idea.Note that the decision tree needs to correctly handle the case when the terminal state has already been reached. Example2.Consider a constraint over vectors of length.First,we need a signature constraint relating each pair of arguments to a signature variable.This can be done as follows: .The automaton of and the decision tree corresponding to the transition constraint are shown in part(A)of Fig.2. Example3.Consider a among constraint.First,we need a signature con-straint among relating each argument to a signature letter.This can be done as follows: among. The automaton of among and the decision tree corresponding to the transition constraint among are shown in part(B)of Fig.2. Consistency.We consider automata where all subsets of variables in are pairwise disjoint,and that do not involve counters.Many constraints can be encoded by such automata,for instance the global lesseq constraints presented in Fig.1.For this kind of automata the?ltering algorithm achieves arc-consistency,provided that the?ltering algorithms of signature and transition constraints achieve also arc-consistency.To prove this property,consider the constraint hypergraph that represents the conjunction of all signature and transition constraints(see Fig.3).It has two particular properties:there is no cycle in the corresponding intersection graph2, and for any pair of constraints the two sets of involved variables share at most one variable.Such an hypergraph is so-called Berge-acyclic[9].Berge-acyclic constraint s Y0 X1 Y1 S0 t $ Y m?1 ......... X0 S1S m?1 X m?1 2 Q 1 Q m?1 Q Q m Fig.3.Constraint hypergraph of the conjunction of transition and signature constraints in the case of disjoint sets.The-th set is denoted by. networks were proved to be solvable polynomially by achieving arc-consistency[21, 22].Therefore,if all signature and transition constraints achieve arc-consistency then we obtain a complete?ltering for our global constraint. Performance.It is reasonable to ask the question whether the?ltering algorithm de-scribed herein performs anywhere near the performance delivered by a hard-coded im-plementation of a given constraint.To this end,we have compared a version of the Balanced Incomplete Block Design problem[19,prob028]that uses a built-in constraint to break column symmetries with a version using our?ltering based on a ?nite automaton for the same constraint.In a second experiment,we measured the time to?nd all solutions to a single constraint.The experiments were run in SICStus Prolog3.11on a600MHz Pentium III.The results are shown in Table1. Table1.Time in seconds for?nding(A)the?rst solution of BIBD instances using built-in vs. simulated,and(B)all solutions to a single built-in vs.simulated constraint. (A)(B) Problem Simulated 0.250 0.570 0.090 2.180 1.670 3.870 1.470 2.770 1.200 Built-in 40.020 0.110 6 2.300 29.530 4Applications of this Technique Designing Filtering Algorithm for Global Constraints.We apply this new method-ology for designing?ltering algorithms for the following fairly large set of global con-straints.We came up with an automaton3for the following constraints: –Unary constraints specifying a domain like in[14]or not constraint[28]. –Counting constraints for constraining the number of occurrences of a given set of values like among[6],atleast[17],atmost[17]or count[14]. –Sliding sequence constraints like change[5],longest change restricts the variable to the maximum number of consecutive variables of for which the binary constraint holds.–Variations around the element constraint[20]like element lesseq[25]or element index. max contiguity[23],group[17], group isolated different or differ at k different and differ at k quad in quad not same all card same all card 3These automata are available in the Appendix.All signature constraints are encoded in order to achieve arc-consistency. 10 and the exactly one constraint holds if exactly one component of takes its value in the set of values . The left-hand part of Fig.4depicts the two automata and respectively as-sociated with the between and the exactly one between the signature variable and the -th component of vectors , and : if ,9if if ,10if if ,11if if ,12if if ,13if if ,14if if ,15if if ,16if if ,17if bo bi ai to ao ti t o i a b t e eo ei tt i i i i i i i i i i i i i i between eEO eEI eLO lEO lEI lLO lLI lLO eLI eLO lEO O EO lO EI eI eO lO LO O LI lI I LO EO eO $ $$ $eEO $ I O O l $ lL $ e E eL lE L $ eE between and exactly_one exactly_one LEGEND l: a L: b e: a $: end g: a E: b G: b one constraints we need to have arc-consistency on 11 between exactly one. Even if both the between and the exactly 4The corresponding code is available in the Appendix.. 12 When these subsets form a partition over the variables of the constraint and when they consist of a single element,this cost is in fact the minimum number of variables to unassign in order to get back to a solution.As in[27],we add a cost variable as an extra argument of the constraint.Our?ltering algorithm?rst evaluates the minimum cost value.Then,according to,it prunes values that cannot belong to a solution. Example6.Consider the constraint global global contiguity constraint,while part(B)gives the multigraph associated with the soft contiguity constraint previously introduced.Each arc is labeled by the condition associated to its correspond-ing transition.Each node contains the name of the corresponding automaton state.Numbers in a node will be explained later on.Infeasible arcs are represented with a dotted line. We now explain how to use the multigraph to evaluate the minimum violation cost and to prune the signature variables according to the maximum allowed violation cost. Evaluating the minimum violation cost can be seen as?nding the path from the source to the sink of that contains the smallest number of infeasible arcs.This can be done by performing a topological sort starting from the source of.While per-forming the topological sort,we compute for each node of the minimum number of infeasible arcs from the source of to.This number is recorded in.At the end of the topological sort,the minimum violation cost we search for,is equal to. Notation1Let be assignable to a signature variable.denotes the minimum violation cost value according to the hypothesis that we assign to. 13 V 0V 1 V 2 V 3 V 4 V 5 V 6 z:1,2z:0,2z:1,1z:1,1z:2,0 z:1,3 V0,V1,V2,V3,V4,V5,V6 s n z 0 1 1 $ $ $ t s:0,1s:0,1s:1,1s:2,0s:2,0s:3,0s:3,0s:4,0 n:0,1n:0,1n:0,1n:1,0n:1,0i:1,0n:1,0t:1,0 1 00 1 1 1 1 1 1 1 1 1 1 1 1 $ $ $ (A) Automaton for global_contiguity (B) Graph of potential executions of the automaton of global_contiguity according to Fig.6.Relaxing the global 6Conclusion and Perspectives The automaton description introduced in this reportcan be seen as a restricted program-ming language.This language is used for writing down a constraint checker,which ver-i?es whether a ground instance of a constraint is satis?ed or not.This checker allows pruning the variables of a non-ground instance of a constraint by simulating all poten-tial executions of the corresponding program according to the current domain of the variables of the relevant constraint.This simulation is achieved by encoding all poten-tial executions of the automaton as a conjunction of signature and transition constraints and by letting the usual constraint propagation deducing all the relevant information. We want to stress the key points of this approach: –Within the context of global constraints,it was implicitly assumed that providing a constraint checker is a much easier task than coming up with a?ltering algorithm. It was also commonly admitted that the design of?ltering algorithms is a dif?cult task which involves creativity and which cannot be automatized.We have shown that this is not the case any more if one can afford to provide a constraint checker.–Non-determinism has played a key role by augmenting programming languages with backtracking facilities[16],which was the origin of logic programming.Non-determinism also has a key role to play in the systematic design of?ltering algo-rithms:?nding a?ltering algorithm can be seen as the task of executing in a non-deterministic way the deterministic program corresponding to a constraint checker and to extract the relevant information which for sure occurs under any circum-stances.This can indeed be achieved by using constraint programming. We?nally present different perspectives of this work. –A natural continuation would be to extend the automaton description in order to get closer to a classical imperative programming language.This would allow reusing directly available checkers in order to systematically get a?ltering algorithm. –Another interesting question is about identifying other structural conditions on the signature and transition constraints that can guarantee arc-consistency for the orig-inal global constraint. Acknowledgements We are grateful to Irit Katriel for suggesting us the use of topological sort for the re-laxation part,and to Christian Bessi`e re for his helpful comments with respect to Berge-acyclic CSP’s. References 1. A.G.Frutos,Q.Liu,A.J.Thiel,A.M.W.Sanner,A.E.Condon,L.M.Smith,and R.M.Corn. Demonstration of a word design strategy for DNA computing on surfaces.Nucleic Acids Research,25:4748–4757,1997. 15 2.J.Amilhastre,H.Fargier,and P.Marquis.Consistency restoration and explanations in dy- namic CSPs–application to con?guration.Arti?cial Intelligence,135:199–234,2002. 3.N.Beldiceanu.Global constraints as graph properties on structured network of elementary constaints of the same type.In R.Dechter,editor,CP’2000,Principles and Practice of Constraint Programming,volume1894of LNCS,pages52–66.Springer-Verlag,2000. 4.N.Beldiceanu.Pruning for the minimum constraint family and for the number of distinct values constraint family.In T.Walsh,editor,CP’2001,Int.Conf.on Principles and Practice of Constraint Programming,volume2239of LNCS,pages211–224.Springer-Verlag,2001. 5.N.Beldiceanu and M.Carlsson.Revisiting the cardinality operator and introducing the cardinality-path constraint family.In P.Codognet,editor,ICLP’2001,Int.Conf.on Logic Programming,volume2237of LNCS,pages59–73.Springer-Verlag,2001. 6.N.Beldiceanu and E.Contejean.Introducing global constraints in https://www.doczj.com/doc/e517997290.html,put. Modelling,20(12):97–123,1994. 7.N.Beldiceanu,Q.Guo,and S.Thiel.Non-overlapping constraints between convex poly- topes.In T.Walsh,editor,Principles and Practice of Constraint Programming(CP’2001), volume2239of LNCS,pages392–407.Springer-Verlag,2001. 8.N.Beldiceanu and E.Poder.Cumulated pro?les of minimum and maximum resource utili- sation.In Ninth Int.Conf.on Project Management and Scheduling,2004. 9. C.Berge.Graphs and hypergraphs.Dunod,Paris,1970. 10. B.Boigelot and P.Wolper.Representing arithmetic constraints with?nite automata:An overview.In Peter J.Stuckey,editor,ICLP’2002,Int.Conf.on Logic Programming,volume 2401of LNCS,pages1–19.Springer-Verlag,2002. 11.S.Bourdais,P.Galinier,and G.Pesant.HIBISCUS:A constraint programming application to staff scheduling in health care.In F.Rossi,editor,CP’2003,Principles and Practice of Constraint Programming,volume2833of LNCS,pages153–167.Springer-Verlag,2003. 12.M.Carlsson and N.Beldiceanu.From constraints to?nite automata to?ltering algorithms. In D.Schmidt,editor,Proc.ESOP2004,volume2986of LNCS,pages94–108.Springer-Verlag,2004. 13.M.Carlsson et al.SICStus Prolog User’s Manual.Swedish Institute of Computer Science, 3.11edition,January200 4.http://www.sics.se/sicstus/. 14.M.Carlsson,G.Ottosson,and B.Carlson.An open-ended?nite domain constraint solver. In H.Glaser,P.Hartel,and H.Kuchen,editors,Programming Languages:Implementations, Logics,and Programming,volume1292of LNCS,pages191–206.Springer-Verlag,1997. 15. C.Flamm,I.L.Hofacker,and P.F.Stadler.RNA in silico:The computational biology of RNA secondary https://www.doczj.com/doc/e517997290.html,plex Syst.,2:5–90,1999. 16.J.Cohen.Non-deterministic algorithms.ACM Computing Surveys,11(2):79–94,1979. 17.COSYTEC.CHIP Reference Manual,v5edition,2003. 18. A.Frisch,B.Hnich,Z.K?z?ltan,I.Miguel,and T.Walsh.Global constraints for lexico- graphic orderings.In Pascal Van Hentenryck,editor,Principles and Practice of Constraint Programming(CP’2002),volume2470of LNCS,pages93–108.Springer-Verlag,2002. 19.I.P.Gent and T.Walsh.CSPLib:a benchmark library for constraints.Technical Report APES-09-1999,APES,1999.https://www.doczj.com/doc/e517997290.html,. 20.P.Van Hentenryck and J.-P.Carillon.Generality vs.speci?city:an experience with AI and OR techniques.In National Conference on Arti?cial Intelligence(AAAI-88),1988. 21.P.Janssen and M-C.Vilarem.Probl`e mes de satisfaction de contraintes:techniques de r′e solution et application`a la synth`e se de peptides.Research Report C.R.I.M.,54,1988. 22.P.J′e gou.Contribution`a l’′e tude des probl`e mes de satisfaction de contraintes:algorithmes de propagation et de r′e solution.Propagation de contraintes dans les r′e seaux dynamiques.PhD Thesis,1991. 23.M.Maher.Analysis of a global contiguity constraint.In Workshop on Symmetry on Rule- Based Constraint Reasoning and Programming,2002.held along CP-2002. 16 https://www.doczj.com/doc/e517997290.html,ano.Constraint and integer programming.Kluwer Academic Publishers,2004.ISBN 1-4020-7583-9. 25.G.Ottosson,E.Thorsteinsson,and J.N.Hooker.Mixed global constraints and inference in hybrid IP-CLP solvers.In CP’99Post-Conference Workshop on Large-Scale Combinatorial Optimization and Constraints,pages57–78,1999. 26.G.Pesant.A regular language membership constraint for sequence of variables.In Workshop on Modelling and Reformulation Constraint Satisfaction Problems,pages110–119,2003. 27.T.Petit,J.-C.R′e gin,and C.Bessi`e re.Speci?c?ltering algorithms for over-constrained prob- lems.In T.Walsh,editor,Principles and Practice of Constraint Programming(CP’2001), volume2239of LNCS,pages451–463.Springer-Verlag,2001. 28.P.Refalo.Linear formulation of constraint programming models and hybrid solvers.In R.Dechter,editor,Principles and Practice of Constraint Programming(CP’2000),volume 1894of LNCS,pages369–383.Springer-Verlag,2000. 29.N.R.Vempaty.Solving constraint satisfaction problems using?nite state automata.In Na- tional Conference on Arti?cial Intelligence(AAAI-92),pages453–458.AAAI Press,1992. 17 A List of Constraints and their Corresponding Automata A.1among(NVAR,VARIABLES,VALUES)[6] NVAR is the number of variables of the collection VARIABLES which take their value in VALUES. ?-among(3, [[var-4],[var-5],[var-5],[var-4],[var-1]], [[val-1],[val-5],[val-8]]). true. %0:not_in(VAR,VALUES) %1:in(VAR,VALUES) among(NVAR,VARIABLES,VALUES):- col_to_list(VALUES,LIST_VALUES), list_to_fdset(LIST_VALUES,SET_OF_VALUES), among_signature(VARIABLES,SIGNATURE,SET_OF_VALUES), automaton(SIGNATURE,_, SIGNATURE,0..1, [source(s),sink(t)], [arc(s,0,s), arc(s,1,s,[C+1]), arc(s,$,t)], [C],[0],[NVAR]). among_signature([],[],_). among_signature([[var-VAR]|VARs],[S|Ss],SET_OF_VALUES):- VAR in_set SET_OF_VALUES#<=>S, among_signature(VARs,Ss,SET_OF_VALUES). A.2atleast(N,VARIABLES,VALUE)[17] At least N variables of the VARIABLES collection are assigned to value VALUE. ?-atleast(2,[[var-4],[var-2],[var-4],[var-5]],4)). true. atleast(N,VARIABLES,VALUE):- N#= among(M,VARIABLES,[[val-VALUE]]). A.3atmost(N,VARIABLES,VALUE)[17] At most N variables of the VARIABLES collection are assigned to value VALUE. ?-atmost(1,[[var-4],[var-2],[var-4],[var-5]],2) true. atmost(N,VARIABLES,VALUE):- N#>=M, among(M,VARIABLES,[[val-VALUE]]). A.4between(As,Xs,Bs)[12] Vector X is lexicographically greater than or equal to vector A and vector X is lexicographically less than or equal to vector B. 18 ?-between([[var-4],[var-2]],[[var-4],[var-2]],[[var-4],[var-3]]). true. %0:A# %1:A# %2:A# %3:A#=X#/\X# %4:A#=X#/\X#=B %5:A#=X#/\X#>B %6:A#>X#/\X# %7:A#>X#/\X#=B %8:other between(As,Xs,Bs):- between_signature(As,Xs,Bs,SIGNATURE), automaton(SIGNATURE,_, SIGNATURE,0..8, [source(s),node(a),node(b),sink(t)], [arc(s,4,s), arc(s,0,t), arc(s,$,t), arc(s,3,a), arc(s,1,b), arc(a,3,a), arc(a,4,a), arc(a,5,a), arc(a,0,t), arc(a,1,t), arc(a,2,t), arc(a,$,t), arc(b,1,b), arc(b,4,b), arc(b,7,b), arc(b,0,t), arc(b,3,t), arc(b,6,t), arc(b,$,t)], [],[],[]). between_signature([],[],[],[]). between_signature([[var-A1]|As],[[var-X1]|Xs],[[var-B1]|Bs],[L1|Ls]):-Adown is A1-1, Aup is A1+1, Bdown is B1-1, Bup is B1+1, filter_cases([(A1+1 (A1 (true->(Bup..sup)-2), (A1 (A1=:=B1->(A1..A1)-4), (A1>B1->(A1..A1)-5), (true->(inf..Adown)-6), (A1>B1->(B1..B1)-7), (A1>B1+1->(Bup..Adown)-8)], Cases), leaf_nodes(Cases,Leaves,L), case(X-L,[X1-L1],[node(-1,X,Cases)|Leaves]), between_signature(As,Xs,Bs,Ls). filter_cases([],[]). filter_cases([(Cond->Case)|L1],[Case|L2]):- call(Cond),!, filter_cases(L1,L2). filter_cases([_|L1],L2):- filter_cases(L1,L2). leaf_nodes([],[],_). leaf_nodes([_-N|Cases],[node(N,L,[N..N])|Nodes],L):- leaf_nodes(Cases,Nodes,L). 19 A.5between one(As,Xs,Bs,VALUES) Vector Xs is lexicographically greater than or equal to vector As and vector Xs is lexicographically less than or equal to vector Bs and exactly one component of vector Xs has a value in the set of values VALUES. ?-between_exactly_one([[var-4],[var-2]],[[var-4],[var-2]],[[var-4],[var-3]], [[val-1],[val-2],[val-6]]). true. %signature:Lb+La where %Lb=0-(A# %1-(A# %2-(A# %3-(A#=X#/\X# %4-(A#=X#/\X#=B) %5-(A#=X#/\X#>B) %6-(A#>X#/\X# %7-(A#>X#/\X#=B) %8-(A#>X#/\X#>B) %La=0-X not in VALUES %9-X in VALUES between_exactly_one(As,Xs,Bs,VALUES):- col_to_list(VALUES,LIST_VALUES), list_to_fdset(LIST_VALUES,Set), Am in_set Set, between_exactly_one_signature(As,Xs,Bs,Ss,Am), automaton(Ss,_, Ss,0..17, [source(eo), node(ei), node(ao), node(ai), node(bo), node(bi), node(to), node(ti), sink(tt)], [arc(eo,4,eo),%eEO arc(eo,3,ao),%eLO arc(eo,1,bo),%lEO arc(eo,0,to),%lLO arc(eo,13,ei),%eEI arc(eo,12,ai),%eLI arc(eo,10,bi),%lEI arc(eo,9,ti),%lLI % arc(ei,4,ei),%eEO arc(ei,3,ai),%eLO arc(ei,1,bi),%lEO arc(ei,0,ti),%lLO arc(ei,$,tt),%$ % arc(ao,3,ao),%eLO arc(ao,4,ao),%eEO arc(ao,5,ao),%eGO arc(ao,0,to),%lLO arc(ao,1,to),%lEO arc(ao,2,to),%lGO arc(ao,12,ai),%eLI arc(ao,13,ai),%eEI arc(ao,14,ai),%eGI arc(ao,9,ti),%lLI arc(ao,10,ti),%lEI arc(ao,11,ti),%lGI % arc(ai,3,ai),%eLO arc(ai,4,ai),%eEO 20 控制软件说明书 PC端软件FTM 安装及应用 系统运行环境： 操作系统中英文Windows 98/2000/ NT/XP/WIN7/ Vista， 最低配置 CPU：奔腾133Mhz 内存：128MB 显示卡：标准VGA，256色显示模式以上 硬盘：典型安装 10M 串行通讯口：标准RS232通讯接口或其兼容型号。 其它设备：鼠标器 开始系统 系统运行前，确保下列连线正常： 1：运行本软件的计算机的RS232线已正确连接至控制器。 2：相关控制器的信号线，电源线已连接正确； 系统运行步骤： 1：打开控制器电源，控制电源指示灯将亮起。 绿色，代表处于开机运行状态；橙色代表待机状态。 2. 运行本软件 找到控制软件文件夹，点击FWM.exe运行。出现程序操作界面： 根据安装软件版本不同，上图示例中的界面及其内容可能会存在某些差别，可咨询我们的相关的售后服务人员。 上图中用红色字体标出操作界面的各部分的功能说明： 1. 菜单区：一些相关的菜单功能选择执行区。 2. 操作区：每一个方格单元代表对应的控制屏幕，可以通过鼠标或键盘的点选，拖拉的方式选择相应控制单元。 3.功能区：包含常用的功能按钮。 4.用户标题区：用户可根据本身要求，更改界面上的标题显示 5.用户图片区：用户可根据本身要求，更改界面上的图片显示，比如公司或工程相关LOGO图片。 6.附加功能区：根据版本不同有不同的附加项目。 7.状态区：显示通讯口状态，操作权限状态，和当前的本机时间，日期等。 如何开始使用 1. 通讯设置 单击主菜单中“系统配置”――》“通讯配置” 选择正确的通讯端口号，系统才能正常工作。 可以设置打开程序时自动打开串口。 2.系统配置 用友T6管理软件操作手册总账日常业务处理 日常业务流程 1、进入用友企业应用平台。 T6 双击桌面上的 如设置有密码，输入密码。没有密码就直接确定。 2、填制凭证进入系统之后打开总账菜单下面的填制凭证。如下图 丄总账［演示版】国B设畫 -二疑证 i :卜0 直接双击填制凭证，然后在弹出凭证框里点增 制单日期可以根据业务情况直接修改，输入附单据数数（可以不输），凭证摘要（在后面的匝可以选择常用摘要），选择科目直接选择（不知道可以选按F2或点击后面的一）, 输入借贷方金额，凭证完后如需继续作按增加自动保存，按保存也可，再按增加 3．修改凭证 填制凭证 证 证 证 总 ￡ ■ 凭 汇 汇 流 没有审核的凭证直接在填制凭证上面直接修改，改完之后按保存。（审核、记帐了凭 证不可以修改，如需修改必须先取消记帐、取消审核）。 4．作废删除凭证只有没有审核、记帐的凭证才可以删除。在“填制凭证”第二个菜单“制单” 下面有 一个“作废恢复”，先作废，然后再到“制单”下面“整理凭证”，这样这张凭证才被彻底删除。 5．审核凭证 双击凭证里的审核凭证菜单，需用具有审核权限而且不是制单人进入审核凭证才能审核（制单单人不能审核自己做的凭证） 选择月份，确定。 再确定。 直接点击“审核”或在第二个“审核”菜单下的“成批审核” 6．取消审核 如上所述，在“成批审核”下面有一个“成批取消审核”，只有没有记帐的凭证才可 以取消审核 7．凭证记账 所有审核过的凭证才可以记帐，未审核的凭证不能记账，在“总帐——凭证——记账” 然后按照提示一步一步往下按，最后提示记帐完成。 8．取消记帐 在“总帐”—“期末”—“对帐”菜单按“ Ctrl+H ” 系统会提示“恢复记帐前状态已被激活”。然后按“总帐”——“凭证”——“恢复 记帐前状态”。最后选“月初状态”，按确定，有密码则输入密码，再确定。 10、月末结转收支 当本月所有的业务凭证全部做完，并且记账后，我们就要进行当月的期间损益结转。 点击：月末转账并选择期间损益结转。 选择要结转的月份，然后单击“全选”。点击确定后 智能窗户控制系统软件V1.0设计说明 目录 前言 (1) 第一章软件总体设计 (1) 1.1. 软件需求概括 (1) 1.2. 定义 (1) 1.3. 功能概述 (1) 1.4. 总体结构和模块接口设计 (2) 第二章控制系统的总体设计 (3) 2.1. 功能设计 (3) 第三章软件控制系统的设计与实现 (5) 3.1. RF解码过程程序设计介绍 (5) 3.2. RF对码过程设计 (6) 3.3. 通信程序设计 (8) 3.4. IIC程序设计介绍 (9) 3.5. 接近开关程序设计 (12) 3.6. 震动开关检测程序设计 (13) 3.7. 墙面按键程序设计 (15) 第四章智能窗户控制系统的设计 (17) 第五章实测与结果说明 (18) 第六章结论 (18) 前言 目的 编写详细设计说明书是软件开发过程必不可少的部分，其目的是为了使开发人员在完成概要设计说明书的基础上完成概要设计规定的各项模块的具体实现的设计工作。 第一章软件总体设计 1.1.软件需求概括 本软件采用传统的软件开发生命周期的方法，采用自顶向下，逐步细化，模块化编程的软件设计方法。 本软件主要有以下几方面的功能 (1)RF遥控解码 (2)键盘扫描 (3)通信 (4)安全检测 (5)电机驱动 1.2.定义 本项目定义为智能遥控窗户系统软件。它将实现人机互动的无缝对接，实现智能关窗，遥控开关窗户，防雨报警等功能。 1.3.功能概述 1.墙体面板按键控制窗户的开/关 2.RF遥控器控制窗户的开/关 3.具有限位，童锁等检测功能 4.实时检测大气中的温湿度，下雨关窗 5.具有防盗，防夹手等安全性能的检测 NC系统培训手册 编制单位：用友软件股份有限公司 中央大客户事业部 目录 一、NC系统登陆 .................................... 二、消息中心管理................................... 三、NC系统会计科目设置 ............................ 四、权限管理....................................... 五、打印模板设置................................... 六、打印模板分配................................... 七、财务制单....................................... 八、NC系统账簿查询 ................................ 九、辅助余额表查询................................. 十、辅助明细账查询................................. 十一、固定资产基础信息设置......................... 十二、卡片管理..................................... 十三、固定资产增加................................. 十四、固定资产变动................................. 十五、折旧计提..................................... 十六、折旧计算明细表............................... 门禁考勤管理软件 使 用 说 明 书 软件使用基本步骤 一．系统介绍―――――――――――――――――――――――――――――2二．软件的安装――――――――――――――――――――――――――――2 三．基本信息设置―――――――――――――――――――――――――――2 １）部门班组设置―――――――――――――――――――――――――3 ２）人员资料管理―――――――――――――――――――――――――3 ３）数据库维护――――――――――――――――――――――――――3 ４）用户管理―――――――――――――――――――――――――――3 四．门禁管理―――――――――――――――――――――――――――――4 １）通迅端口设置―――――――――――――――――――――――――4２）控制器管理――――――――――――――――――――――――――4３）控制器设置――――――――――――――――――――――――――6４）卡片资料管理―――――――――――――――――――――――――11 ５）卡片领用注册―――――――――――――――――――――――――12６）实时监控―――――――――――――――――――――――――――13 五．数据采集与事件查询――――――――――――――――――――――――13 六．考勤管理―――――――――――――――――――――――――――――14 1）班次信息设置――――――――――――――――――――――――――14 2）考勤参数设置――――――――――――――――――――――――――15 3）考勤排班――――――――――――――――――――――――――――15 4）节假日登记―――――――――――――――――――――――――――16 5）调休日期登记――――――――――――――――――――――――――16 6）请假/待料登记―――――――――――――――――――――――――17 7）原始数据修改――――――――――――――――――――――――――17 8）考勤数据处理分析――――――――――――――――――――――――17 9）考勤数据汇总―――――――—――――――――――――――――――18 10）考勤明细表—―――――――――――――――――――――――――18 11）考勤汇总表――――――――――――――――――――――――――18 12）日打卡查询――――――――――――――――――――――――――18 13）补卡记录查询—――――――――――――――――――――――――19 开票端操作说明 双击桌面“博思开票”图标，单击“确定”，进入开票界面： 一、开票： 日常业务——开票——选择票据类型——增加——核对票号无误后——单击“请核对票据号”——输入“缴款人或缴款单位”——选择”收费项目”、“收入标准”——单击“收费金额”。 （如需增加收费项目，可单击“增一行”） （如需加入备注栏（仅限于收款收据）），则在右侧“备注”栏内输入即可） 确认无误后，单击“打印”——“打印” 二、代收缴款书： 日常业务——代收缴款书——生成——生成缴款书——关闭——缴款——输入“专用票据号”——保存——缴款书左上角出现“已缴款”三个红字即可。 三、上报核销： 日常业务——上报核销——选择或输入核销日期的截止日期——刷新——核销。 （注意：“欠缴金额”处无论为正或为负均不可核销，解决方法见后“常见问题”） 常见问题 一、如何作废“代收缴款书” 日常业务——代收缴款书——缴款——删除“专用票据号”和“缴款日期”——保存——作废。 二、上报核销时出现欠缴金额，无法完成核销，或提示多缴。 1、首先检查有没有选择好截止日期，选择好后有没有点击“刷新”。 2、其次检查有没有做代收缴款书。注意：最后一张缴款书的日期不得晚于选择上报核 销日期。 3、若上述方法仍无效，则可能是由于以前作废过票据而未作废缴款书。解决方法： 首先作废若干张缴款书（直到不能作废为止），然后重新做一张新的缴款书。再核销。 三、打开“博思开票”时，出现“windows socket error：由于目标机器积极拒绝，无法连接。 （10061），on API’connect’” 单击“确定”，将最下面一行的连接类型“SOCKET”更换为“DCOM”，再点“连接” 即可。 四、如何设置密码 双击桌面“博思开票”，单击登录界面的右下方“改口令”输入用户编号、新密码和确认密码，单击“确认”即可。 五、更换开票人名称或增加开票人 进入开票系统——系统维护——权限管理 1、更换开票人名称：单击“用户编码”——删除“用户名”——输入新的开票人名称 ——单击“保存用户”即可。 2、增加开票人：单击“新增用户”——输入“用户编码”和“用户名”——单击“保 存用户”——单击新增的用户编码——将右边的“权限列表如下”下面的“所有”前的小方框勾上——单击右侧“保存用户权限”。 六、重装电脑系统 1、由于博思开票软件安装在D盘，所以重装电脑系统前无需做任何备份。 2、重装系统后，打开我的电脑—D盘，将“博思软件”文件夹复制到桌面上（或U盘）。 3、将安装时预留的安装光盘放入主机，打开后找到“票据核销及管理_开票端(江西欠 缴不能上报版)”（或者进入D盘----开票软件备份目录勿删文件夹里也可找到）。双 击，按提示点击“下一步”，直到“完成”。 4、双击桌面任务栏右下角“博思开票服务器”，将其关闭（或右键点击“博思开票服 务器”——“关闭服务器”）。 （这一步若找不到“博思开票服务器”，也可以用重启电脑来代替） 5、将刚才复制到桌面（或U盘）的“博思软件”再复制粘贴回D盘，若提示“此文 件夹已包含名为博思软件的文件夹”，点击下面的“全部”。 6、双击桌面“博思开票”——输入用户编码(001)——确定。 7、确认原来的票据数据没有丢失后，将桌面（或U盘）的“博思软件”文件夹删除。 控制系统使用说明 系统针对轴流风机而设计的控制系统, 系统分为上位监视及下位控制两部分 本操作为上位监控软件的使用说明: 1: 启动计算机: 按下计算机电源开关约2秒, 计算机启动指示灯点亮, 稍过大约20秒钟屏幕出现操作系统选择菜单, 通过键盘的“↑↓”键选择“windows NT 4.0”菜单，这时系统进入WINDOWS NT 4.0操作系统，进入系统的操作画面。 2：系统操作 系统共分：开机画面、停机画面、趋势画面、报警画面、主机流程画面、轴系监测画面、润滑油站画面、动力油站画面、运行工况画面、运行记录画面等十幅画面，下面就十幅画面的作用及操作进行说明 A、开机画面： 开机： 当风机开始运转前，需对各项条件进行检查，在本画面中主要对如下指标进行检查，红色为有效： 1、静叶关闭：静叶角度在14度 2、放空阀全开：放空阀指示为0% 3、润滑油压正常 4、润滑油温正常 5、动力油压正常 6、逆止阀全关 7、存储器复位：按下存储器复位按钮，即可复位，若复位不成 需查看停机画面。 8、试验开关复位：按下试验开关按钮即可，试验开关按钮在风 机启动后，将自动消失，同时试验开关也自动复位。 当以上条件达到时，按下“允许机组启动”按钮，这时机组允许启动指示变为红色，PLC机柜里的“1KA”继电器将导通。机组允许启动信号传到高压柜，等待电机启动。开始进行高压合闸操作，主电机运转，主电机运转稳定后，屏幕上主电机运行指示变红。这时静叶释放按钮变红，按下静叶释放按钮后，静叶从14度开到22度，静叶释放成功指示变红。 应继续观察风机已平稳运行后，按下自动操作按钮，启机过程结束。 B、停机画面： 停机是指极有可能对风机产生巨大危害的下列条件成立时，PLC 会让电机停止运转： 1、风机轴位移过大 用 友 T+ 软 件 系 统 操 作 手 册版本号：v1.0 目录 一、系统登录 (3) 1.1、下载T+浏览器 (3) 1.2、软件登陆 (3) 二、基础档案设置 (5) 2.1、部门、人员档案设置 (5) 2.2、往来单位设置 (6) 2.3、会计科目及结算方式设置 (6) 三、软件操作 (9) 3.1、凭证处理 (9) 3.1.1、凭证填制 (9) 3.1.2、凭证修改 (10) 3.1.3、凭证审核 (11) 3.1.4、凭证记账 (12) 3.2、月末结转 (13) 四、日常帐表查询与统计 (14) 4.1、余额表 (14) 4.2、明细账 (15) 4.3、辅助账 (16) 五、月末结账、出报表处理 (17) 5.1、总账结账 (17) 5.2、财务报表 (20) 一、系统登录 1.1、下载T+浏览器 首次登陆需要用浏览器打开软件地址，即：127.0.0.1:8000(一般服务器默认设置，具体登陆地址请参考实际配置)，第一次登陆会提示下载T+浏览器，按照提示下载安装T+浏览器，然后打开T+浏览器，输入软件登陆地址。 ，T+浏览器， 1.2、软件登陆 按键盘上的“回车键（enter）”打开软件登陆页面，如下： 选择选择“普通用户”，输入软件工程师分配的用户名和密码，选择对应的账套，以下以demo 为例，如下图： 点击登陆，进入软件， 二、基础档案设置 2.1、部门、人员档案设置 新增的部门或者人员在系统中可按照如下方法进行维护， 2.2、往来单位设置 供应商客户档案的添加方法如下： 添加往来单位分类： 2.3、会计科目及结算方式设置会计科目： LED-ECS编辑控制系统V5.2 用 户 手 册 目录 第一章概述 (3) 1.1LED-ECS编辑控制系统介绍 (3) 1.2运行环境 (3) 第二章安装卸载 (3) 2.1安装 (3) 2.2卸载 (5) 第三章软件介绍 (5) 3.1界面介绍 (5) 3.2操作流程介绍 (13) 3.3基本概念介绍 (21) 第四章其他功能 (25) 4.1区域对齐工具栏 (25) 4.2节目对象复制、粘贴 (26) 4.3亮度调整 (26) 第五章发送 (27) 5.1发送数据 (27) 第六章常见问题解决 (28) 6.1计算机和控制卡通讯不上 (28) 6.2显示屏区域反色或亮度不够 (29) 6.3显示屏出现拖尾现象，显示屏的后面出现闪烁不稳定 (29) 6.4注意事项 (31) 6.5显示屏花屏 (31) 6.6错列现象 (32) 6.7杂点现象 (32) 第一章概述 1.1LED-ECS编辑控制系统介绍 LED-ECS编辑控制系统，是一款专门用于LED图文控制卡的配套软件。其具有功能齐全，界面直观，操作简单、方便等优点。自发布以来，受到了广大用户的一致好评。 1.2运行环境 ?操作系统 中英文Windows/2000/NT/XP ?硬件配置 CPU:奔腾600MHz以上 内存:128M 第二章安装卸载 2.1LED-ECS编辑控制系统》软件安装很简单，操作如下：双击“LED-ECS编辑控制系统”安装程序，即可弹出安装界面，如图2-1开始安装。如图所示 图2-1 单击“下一步”进入选择安装路径界面，如图2-2，如果对此不了解使用默认安装路径即可 图2-2 图2-3 单击“完成”，完成安装过程。 2.2软件卸载如图2-2 《LED-ECS编辑控制系统V5.2》提供了自动卸载功能，使您可以方便的删除《LED-ECS编辑控制系统V5.2》的所有文件、程序组件和快捷方式。用户可以在“LED-ECS编辑控制系统V5.2”组中选择“卸载LED-ECS编辑控制系统V5.2”卸载程序。也可以在“控制面板”中选择“添加/删除程序”快速卸载。卸载程序界面如图2-4，此时选择自动选项即可卸载所有文件、程序组和快捷方式。 图2-4 第三章、软件介绍 财政票据(网络版)电子化系统 开票端 操 作 说 明 福建博思软件股份有限公司 目录 1.概述 业务流程 流程说明： 1.单位到财政部门申请电子票据，由财政把单位的基本信息设置好并审核完后，财政部门给用票单位发放票据，单位进行领票确认并入库。 2.在规定时间内，单位要把开据的发票带到财政核销，然后由财政进行审核。 系统登录 登入系统界面如图： 登录日期：自动读取主服务器的日期。 所属区划：选择单位所属区划编码。【00安徽省非税收入征收管理局】 所属单位：输入单位编码。 用户编码：登录单位的用户编码【002】 用户密码：默认单位密码为【123456】 验证码：当输入错误时，会自动换一张验证码图片； 记录用户编码：勾选系统自动把用户编码保存在本地，第二次登录不需要重新输入。 填写完正确信息，点【确定】即可登入系统。 进入系统 进入系统界面如图： 当单位端票据出现变动的时候，如财政或上级直管下发票据时，才会出现此界面: 出现此界面后点击最下方的确认按钮，入库完成。 当单位端票据无变动时，直接进入界面： 2.基本编码人员管理 功能说明：对单位开票人员维护，修改开票人名称。 密码管理 修改开票人员密码，重置等操作。 收发信息 查看财政部门相关通知等。 3.日常业务 电脑开票 功能说明：是用于开票据类型为电子化的票据。 在电脑开票操作界面，点击工具栏中的【增加】按钮，系统会弹出核对票号提示框，如图： 注意：必须核对放入打印机中的票据类型、号码是否和电脑中显示的一致，如果不一致打印出来的票据为无效票据，核对完后，输入缴款人或缴款单位和收费项目等信息，全部输入完后，点【增加】按钮进行保存当前票据信息或点【打印】按钮进行保存当前票据信息并把当前的票据信息打印出来；点电脑开票操作界面工具栏中的【退出】则不保存。 在票据类型下拉单框中选择所要开票的票据类型，再点【增加】进行开票。 用友T软件系统操作手 册 Pleasure Group Office【T985AB-B866SYT-B182C-BS682T-STT18】 用 友 T+ 软 件 系 统 操 作 手 册 版本号：目录 一、系统登录 、下载T+浏览器 首次登陆需要用浏览器打开软件地址，即：(一般服务器默认设置，具体登陆地址请参考实际配置)，第一次登陆会提示下载T+浏览器，按照提示下载安装T+浏览器，然后打开T+浏览器，输入软件登陆地址。 ，T+浏览器， 、软件登陆 按键盘上的“回车键（enter）”打开软件登陆页面，如下： 选择选择“普通用户”，输入软件工程师分配的用户名和密码，选择对应的账套，以下以demo为例，如下图： 点击登陆，进入软件， 二、基础档案设置 、部门、人员档案设置 新增的部门或者人员在系统中可按照如下方法进行维护， 、往来单位设置 供应商客户档案的添加方法如下： 添加往来单位分类： 、会计科目及结算方式设置 会计科目： 系统预置170个《2013小企业会计准则》科目，如下： 结算方式，如下： 三、软件操作 、凭证处理 填制 进入总账填制凭证菜单，增加凭证，填制摘要和科目，注意有辅助核算的会计科目， 以下为点开总账的处理流程图： 如若现金流量系统指定错误，可按照以下步骤修改： 凭证在没有审核时，可以直接在当前凭证上修改，然后点击“保存”完成修改； 凭证审核 进入总审核凭证菜单下，如下图： 选择审核凭证的会计期间： 、凭证记账 进入凭证菜单下的记账菜单， 、月末结转 期间损益结转 四、日常帐表查询与统计 、余额表 用于查询统计各级科目的本期发生额、累计发生额和余额等。传统的总账，是以总账科目分页设账，而余额表则可输出某月或某几个月的所有总账科目或明细科目的期初余额、本期发生额、累计发生额、期末余额，在实行计算机记账后，我们建议用户用余额表代替总账。 创维液晶拼接控制系统 软件操作指南 【LCD-CONTROLLER12】 请在使用本产品前仔细阅读该用户指导书 温馨提示:: 温馨提示 ◆为了您和设备的安全，请您在使用设备前务必仔细阅读产品说明书。 ◆如果在使用过程中遇到疑问,请首先阅读本说明书。 正文中有设备操作的详细描述,请按书中介绍规范操作。 如仍有疑问,请联系我们,我们尽快给您满意的答复。 ◆本说明书如有版本变动,恕不另行通知,敬请见谅！ 一、功能特点 二、技术参数 三、控制系统连接示意图 四、基本操作 五、故障排除 六、安全注意事项 一、功能特点创维创维--液晶液晶拼接拼接拼接控制器特点控制器特点 ★采用创维第四代V12数字阵列高速图像处理技术 视频带宽高达500MHZ，应用先进的数字高速图像处理算实时分割放大输入图像信号，在多倍分割放大处理的单屏画面上，彻底解决模/数之间转换带来的锯齿及马赛克现象，拼接画面清晰流畅，色彩鲜艳逼真。 ★具有开窗具有开窗、、漫游漫游、、叠加等功能 以屏为单元单位的前提下，真正实现图像的跨屏、开窗、画中画、缩放、叠加、漫游等个性化功能。 ★采用基于LVDS 差分传送技术差分传送技术，，增强抗干扰能力 采用并行高速总线连接技术，上位控制端发出命令后，系统能快速切换信号到命令指定的通道，实现快速响应。 采用基于LVDS 差分传送技术，提高系统抗干扰能力，外部干扰对信号的影响降到了最低，并且，抗干扰能力随频率提高而提升。★最新高速数字阵列矩阵通道切换技术 输入信号小于64路时，用户不需要再另外增加矩阵，便可以实现通道之间的任意换及显示。 ★断电前状态记忆功能 通过控制软件的提前设置，能在现场断电的情况下，重启系统后，能自动记忆设备关机前的工作模式状态。 ★全面支持全高清信号 处理器采用先进的去隔行和运动补偿算法，使得隔行信号在大屏幕拼接墙上显示更加清晰细腻，最大限度的消除了大屏幕显示的锯齿现象，图像实现了完全真正高清实时处理。纯硬件架构的视频处理模块设计，使得高清视频和高分辨率计算机信号能得到实时采样，确保了高清信号的最高视频质量，使客户看到的是高质量的完美画质。 工会经费收入专用收据(1) 福州博思软件开发有限公司 2010年6月 目录 第一部分初始安 装 ....................................................... (1) 1.1系统 安装 (1) 1.2系统登录 ............................................................ (4) 第二部分组成模块介 绍 ................................................... (4) 2.1模块组 成 (4) 2.1.1票据资料 .......................................................... (5) 2.1.2用户管 理 .......................................................... (5) 2.1.3 票据领用 (6) 2.1.4电脑开票 .......................................................... (6) 2.1.5手工开 票 .......................................................... (7) 2.1.6 手工批开票 (7) 2.1.7票据查询 .......................................................... (8) 第三部分软件操 作 ....................................................... (9) 3.2用户 管理 (10) 大屏幕控制系统软件详解说明 一软件安装 安装注意事项： 非专业人事安装：安装前请先关闭防火墙（如360安全卫士，瑞星，诺盾等），等安装完并且成功启动本软件后可重新开启防火墙； 专业人事安装：先把防火墙拦截自动处理功能改为询问后处理，第一次打开本软件时会提示一个拦截信息； 安装前请校对系统时间,安装后不能在错误的系统时间下运行/启动软件,否则会使软件注册失效，这种情况下需要重新注册； Windows 7,注意以下设置 0.1)打开控制面板 0.2) 选择系统和安全 0.3) 选择操作中心 0.4) 选择更换用户帐户控制设置 0.5)级别设置，选择成从不通知 １．软件解压后，请选择双击，进入安装界面如图１，图２ 图1 图2 ２．选择键，进入下一界面如图3 图３ 3.选中项，再按键，进入下一界面如图４ 图4 4.选择键，进入下一界面如图５ 图５ ５.选中项，再选择键，进入下一界面如图６ 图６ ６.选择键，进入下一界面如图７ 图８ ７.选择键，软件安装完成 二软件操作 选择WINDOWS 下开始按钮，选择程序，选择Wall Control项， 点击Wall Control软件进入大屏幕控制系统软件主界面如图9所示,整个软件分为3个区，标题区，设置区，功能区 图9 1.1标题区 大屏幕控制系统软件(只有管理员才可设置此项目) 1.2设置区 1.2.1系统 高级功能：管理员登录。 产品选型：选择拼接盒型号。 定时系统：设置定时时间。 幕墙开机：开机 幕墙关机：关机 退出：退出软件系统。 1.2.2设置 串口设置：设置使用的串口参数。 矩阵设置：设置矩阵的相关参数。 幕墙设置：幕墙设置参数。 幕墙颜色：幕墙颜色设置。 标志设置：更改幕墙名称。 系统设置：控制软件系统设置。 1.2.3工具 虚拟键盘：虚拟键盘设置。 硬件注册：可以通过时钟IC注册处理器的使用权限。 1.2.4语言 中文选择:选择软件语言类型为中文。 Ｅnglish:选择软件语言类型为英语。 用友财务管理系统操作手册 北京用友政务软件有限公司 2011年05月25日 一、账务系统： 流程：1、初始化设置及期初数装入=》2、凭证录入=》 3、凭证审核=》 4、凭证记账=》 5、月结 1、初始化设置: (1)、用自己的用户名登录【账务管理系统】=》 点击界面右边【基础资料】前的【+】号=》点击【会计科 目】前的【+】号=》双击【建立会计科目】=》设置会计科 目及挂接辅助账。(2)、点击界面右边【账务】前的【+】号 =》点击【初始建账数据】前的【+】号=》双击【期初余额 装入】=》点击【确定】=》然后对期初数据进行录入 2、凭证录入:用自己的用户名登录【账务管理系统】=》点击界 面右边【账务】前的【+】号=》点击【凭证管理】前的【+】 号=》双击【编制凭证】=》然后在【编制凭证】界面录入 收入/支出的凭证。 3、凭证审核：点击界面右边【账务】前的【+】号=》点击【凭 证管理】前的【+】号=》双击【凭证处理】=》选中需要审 核凭证的日期=》在左下角选择凭证的状态【未审核】=》 点击右键全选=》点击【审核】； 4、凭证记账：点击界面右边【账务】前的【+】号=》点击【期 末处理】前的【+】号=》双击【凭证处理】=》选中需要记 账凭证的日期=》在左下角选择凭证的状态【已审核】=》 点击右键全选=》点击【记账】； 5、月结：点击界面右边【账务】前的【+】号=》点击【期末 处理】前的【+】号=》双击【期末处理向导】=》点击【结 账向导】=》全部点击【下一步】=》下到最后点击【完成】 二、电子系统： 1、输出单位资产负债表：双击【电子报表系统】=》【管理员】 登录=》在右上角【报表数】下点击【基本户】/【专账一】 /【专账二】下前的【+】号=》双击【资产负债表】=》点击 最右上面【数据】下=》=》点击【登录数据库】=》双击【账 务系统】=》用自己的用户进行登录=》如果图片闪烁就证 明已经登录=》点击【退出】=》点击最右上角找到【插入】 功能菜单=》点击【表页】=》选择出报表的最后日期(如1 月：则时间2011年1月31日)=》选择复制指定表页 =》点击放大镜=》选择【本公司】=》选中【格式】点击【确定】=》在点【确定】=》左 下角有【第201101期】=》点击编制【眼睛图标】。=》调 试报表=》点击【保存】=》打印报表。 2、输出单位支出明细表：双击【电子报表系统】=》【管理员】 登录=》在右上角【报表数】下点击【基本户】/【专账一】 /【专账二】下前的【+】号=》双击【支出明细表】=》点击 最右上面【数据】下=》=》点击【登录数据库】=》双击【账 务系统】=》用自己的用户进行登录=》如果图片闪烁就证 明已经登录=》点击【退出】=》点击最右上角找到【插入】 目录 1，系统概述--------------------------------------------------------------------------------------------------1 1.1 系统简介---------------------------------------------------------------------------------------------2 1.2 系统主要组成---------------------------------------------------------------------------------------2 1.3 系统硬件简要连接图------------------------------------------------------------------------------3 1.4 实际连线图------------------------------------------------------------------------------------------3 2,系统软件使用软件简要说明-----------------------------------------------------------------------------5 2.1 介绍---------------------------------------------------------------------------------------------------5 2.2 操作步骤---------------------------------------------------------------------------------------------5 2.3 取景窗口---------------------------------------------------------------------------------------------7 2.4 flash/cel文件的播放--------------------------------------------------------------------------------7 注1:连接网络的相关设置修改--------------------------------------------------------------9 注2:本机IP的查询----------------------------------------------------------------------------9 注3:本机IP的修改----------------------------------------------------------------------------10 注4:控制器IP的修改-------------------------------------------------------------------------11 3,对应表制作与选择-----------------------------------------------------------------------------------------12 3.1 介绍---------------------------------------------------------------------------------------------------12 3.2 操作步骤---------------------------------------------------------------------------------------------12 4,说明-----------------------------------------------------------------------------------------------------------14 4.1 ONC1A------------------------------------------------------------------------------------------------14 4.2 ONC1B------------------------------------------------------------------------------------------------14 4.3 ONC1C------------------------------------------------------------------------------------------------15 4.4 ONC1D------------------------------------------------------------------------------------------------15 4.5 ONC1E------------------------------------------------------------------------------------------------16 4.6 ONC1F------------------------------------------------------------------------------------------------17 4.7 ONC1G------------------------------------------------------------------------------------------------17 4.8 ONC1F------------------------------------------------------------------------------------------------17 5,附件-----------------------------------------------------------------------------------------------------------19 5.1 数码按钮控制板说明--------------------------------------------------------------------------------19 5.2 象素点排列说明--------------------------------------------------------------------------------------19 政府采购网上公开信息系统供应商操作指南 福建博思软件股份有限公司 2017年06月 目录 1. CA办理 (4) 1.1 CA办理 (4) 1.2 CA盖章 (4) 2. 系统注册 (4) 2.1系统注册 (4) 2.2 注册成功，供应商登录 (5) 3.系统基础操作 (6) 3.1 CA控件下载 (6) 3.2进行政府采购活动 (9) 3.3 供应商资料维护 (10) 3.4 供应商项目报名 (11) 3.5供应商用户管理 (11) 4．投标流程 (11) 4.1项目报名 (11) 4.2 投标文件编制 (13) 4.2.1客户端安装 (13) 4.2.2投标客户端路径修改 (15) 4.2.3应答 (16) 4.2.4标书加密 (21) 4.2.5接着点击退出系统 (21) 4.3投标文件上传： (22) 4.4合同签订： (23) 4.5验收申请： (23) 1.CA办理 供应商须办理福建省CA，进行政府采购活动 1.1CA办理 可登陆https://www.doczj.com/doc/e517997290.html,/或者联系客服0591-968975。 1.2CA盖章 CA盖章操作系统为：XP(SP2)不支持（浏览器目前测试都支持）。 2. 系统注册 2.1系统注册 登入福建省政府采购网https://www.doczj.com/doc/e517997290.html,/，找到登陆与注册进行供应商注册 2.2 注册成功，供应商登录 注：原省网已注册的供应商已完成迁移，请各供应商使用注册时的组织机构代码登录，密码初始为1。 3.系统基础操作 3.1 CA控件下载与安装 登录之前可先进行CA控件下载 (1)打开ISignature,点击installer.exe进行安装 用友财务软件操作流程手册 系统管理 一增加操作员 1、系统管理→系统→注册→输入用户名（admin）→无密码→确定 2、单击权限→操作员→点增加→输入编号、姓名、口令→点增加 二、建新账套 1、系统管理→系统→注册→输入用户名（admin）→无密码→确定 2 单击帐套→建立→输入帐套号、帐套名称、→设置会计期间→下一步→ 输入单位名称→下一步→选择企业类型（工业类型比商业类型多产成品入库单，和材料出库单）→行业性质→选择帐套主管→在“行业性质预置科目”前面打钩则系统将预置所选行业会计科目（否则不予预置）→下一步→如需分类在项目前面方框内打钩→下一步→完成 三、分配权限 1、系统管理→系统→注册→输入用户名（admin）→无密码→确定 2、赋权限的操作顺序： A 受限，明细权限设置权限”-→“权限”菜单→首先选择所需的账套→选操作员→点增加 B 帐套主管权限设置选择所需帐套→再选操作员→在帐套主管前面直接打钩 四、修改账套 1、以“账套主管（不是admin）”身份进入“系统管理”模块（进入系统服务→系统管理→注册） 2、单击帐套→修改 五．备份 打开系统管理→系统→注册admin →帐套→备份→选择存放路径 六．恢复 系统管理→系统→注册→admin →帐套→恢复（选择本分文件的路径，lst为后缀名的文件）总帐系统 初始化 一、启用及参数设置 二、设置“系统初始化”下的各项内容（其中：最后设置会计科目和录入期初余额，其余各项从上向 下依次设置） 1 会计科目设置 1、指定科目 系统初始化→会计科目→编辑（菜单栏中的）→指定科目 现金总帐科目把现金选进以选科目 银行总帐科目把银行存款选进已选科目 动环监控软件操作 手册 深圳市通讯威科技有限公司 EP-MEVP SYSTEM 动力环境集中监控系统 安装使用说明书 版本 2.0 目录 第一章软件的安装卸载升级 ................................. 错误!未定义书签。 1.1软件安装对计算机的配置要求........................ 错误!未定义书签。 1.2软件的安装 ....................................................... 错误!未定义书签。 1.3软件的卸载 ....................................................... 错误!未定义书签。 1.4软件的升级 ....................................................... 错误!未定义书签。第二章软件的基本操作 .......................................... 错误!未定义书签。 2.1登录和进入软件操作界面................................ 错误!未定义书签。 2.2添加/设置/修改/删除硬件设备以及参数设置错误!未定义书签。 2.2.1添加/设置控制器、采集器参数................. 错误!未定义书签。 2.2.2修改/删除硬件设备 .................................... 错误!未定义书签。 2.3监控设置及记录查询 ....................................... 错误!未定义书签。 2.3.1报警方式定义 ............................................. 错误!未定义书签。 2.3.2语音电话报警 ............................................. 错误!未定义书签。 2.3.3短信报警 ..................................................... 错误!未定义书签。 2.3.4监控实时记录 ............................................. 错误!未定义书签。 2.3.5监控报警记录 ............................................. 错误!未定义书签。 2.3.6温湿度数据记录.......................................... 错误!未定义书签。 2.3.7 UPS监控数据记录 ...................................... 错误!未定义书签。 2.3.8 电话短信报警数据记录 .............................. 错误!未定义书签。 2.3.9 空调监控数据记录...................................... 错误!未定义书签。
相关主题
文本预览