Specifying and Verifying Fairness Enhanced Systems

\n<<<\n* Dr. [[SUN, Jun|http://www.comp.nus.edu.sg/~sunj]], Research Fellow, School of Computing, National University of Singapore.\n* Dr. [[DONG, JinSong|http://www.comp.nus.edu.sg/~dongjs/]], Associated Professor, School of Computing, National University of Singapore.\n* Mr. [[LIU Yang|http://www.comp.nus.edu.sg/~liuyang]], PhD Candidate, School of Computing, National University of Singapore.\n* Dr. [[WANG Hai|http://users.ecs.soton.ac.uk/hw/]], Research Fellow, School of Electronics and Computer Science, University of Southampton\n<<<\n

<HTML>\n<HEAD>\n<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">\n</HEAD>\n\nThe Algorithms for the feasible test are shown as follows.\n<CENTER>\n<IMG SRC="algo1.JPG" BORDER="0" ALT="">\n</CENTER>\n\nThe Algorithm for model checking is shown as follows.\n<CENTER>\n<IMG SRC="algo2.JPG" BORDER="0" ALT="">\n</CENTER>\n</HTML>\n

* [[Dining Philosophers]]\n* [[Peterson's Algorithm]]

* Line Number Display.\n* Syntax Highlight with Configuration File.\n* Multi Documents Working Enviroment.\n* Various Shortcuts Editing Function.

<HTML>\n<HEAD>\n<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">\n</HEAD>\n<CENTER>\n<IMG SRC="dp.JPG" BORDER="0" ALT="">\n</CENTER>\n</HTML>\n

<HTML>\nThe weak fairness wf(e) asserts that if an event e eventually\nbecomes enabled forever, infinitely many occurrences of the event\nsteps must be observed. The strong fairness sf(e) asserts that if\ne is infinitely often enabled, infinitely many occurrences of the\nevent must be observed. Strong fairness implies weak fairness. A\nsystem satisfies a fairness constraint if and only if every run of\nthe system satisfies the fairness constraint. The following defines\nenabledness in our setting.\n\n<CENTER>\n<IMG SRC="definition34.JPG" BORDER="0" ALT="">\n</CENTER>\n\n</HTML>\n\n!''Live Event''\n<HTML>\n\nWeak fairness means that if an event is enabled forever, then it\nmust eventually be engaged. In reality, not all events are required\nto get engaged eventually if enabled continuously. For instance, the\naction of inserting a coin may never occur in the vending machine\nexample if the machine is located in a far-away desert, although it\nmay be enabled forever. Nevertheless, once a coin has been inserted\nand an item has been selected, a reasonable expectation is that the\nvending machine should eventually dispatch the requested item. Our\nremedy to the lacking of fairness in safety-centric languages like\nCSP is to mark some of the events as live events.A live event is written as e. Let &#X3A3; be\nthe set of all live events. e plays the same role as e\nexcept that it carries a fairness constraint, though it is\nconsidered as a different event from e. A live event must be\nengaged eventually if it is enabled forever. A similar notion has\nbeen studied in CCS and in CSP. There are, however, important\nsemantic differences between the previous ones and ours (see below).\nIn order to clarify the semantics of live events, two important\nquestions need to be answered. First, because live events may\nsynchronize with live events or ordinary events following the rules\nin Figure 1, one question is that whether the synchronization of a\nlive event and an ordinary event results in a live event or not. For\nexample, if we mark request1 in process Agent1 as a live\nevent, is the event required to occur eventually in process\nSystem? The answer to the question determines how fairness\nconstraints will be distributed in concurrent processes. If a\nfairness constraint is forgotten after synchronization, in order to\nguarantee the specification satisfies the fair constraint, all\noccurrences of the event in different system components must be\nmarked live. For instance, request1 in Agent1 and Sem must\nbe marked as live so that request1 is eventually engaged in\nSystem. This approach is adapted in some work without explicitly\nstated. It is not adapted in this works for serval reasons. Firstly,\nit requires more markings. Secondly, it will be difficult to tell if\na shared event will be enabled or not in a complex system design\n(which depends on coordination of different system components), and\ntherefore it is difficult for system designers to grasp the system\nbehaviors, i.e., whether an event marked live is eventually engaged.\nThirdly, it is sometimes un-natural. For instance, it is natural for\nan agent to require that its request is eventually served, whereas\nit may not be so for the semaphore to require eventually there is a\nrequest from certain agent. The other question is whether the system\nis required to move beyond a state where there is a choice of both\nlive and ordinary events. For instance, is &#X27E8;\nupdate_nonshared &#X27E9; &#X3C9; is a fair trace of Agent4\n&#X2225; Agent3 where Agent3 defined in\nExample 1 and Agent4 = e1 &#X2192; Agent4 | e2\n&#X2192; Stop? Firstly, by Definition , (Agent4\n&#X2225; Agent3, &#X2205;, &#X27E8; update_nonshared &#X27E9;&#X3C9;) &#X22AD;wf(e1). Secondly,\nwe believe that semantically there is no distinction between\nconcurrent or sequential processes.\n\n<CENTER>\n<IMG SRC="definition5.JPG" BORDER="0" ALT="">\n</CENTER>\n\nThe definition above defines readyness, which is a centric\nidea in our approach. Intuitively, an event is ready if and\nonly if one thread of control is ready to engage in it. An\nenabled event must be ready. Note that\nenabledness and readyness are equivalent for all\nprocess expressions except parallel composition. An event is\nready in process P1\n&#X2225; P2 if it is enabled by one (or more) of the\ncomponents, even if it must be synchronized by multiple processes\nand some of them are not ready. While a shared event is\nenabled in P1 &#X2225; P2 if and only if it is enabled in both\nP1 and P2.\n\n<CENTER>\n<IMG SRC="definition6.JPG" BORDER="0" ALT="">\n</CENTER>\n\nCompared to Definition 2, the additional constraint states that an\ninfinite sequence of events is a trace of the process only if\nwhenever there is a live event ready, it must be either\nengaged or become not ready after one or more transitions. By\ndefinition, the synchronization of two events is a live event if and\nonly if at least one of the events is a live event. The intuition is\nthat the synchronized event shall not forget the fairness\nconstraint. Semantically, this approach allows us to localize\nfairness constraints to the relevant system components. The\nfollowing claims the soundness of live events (which can be proved\nby Definition 6).\n\n<CENTER>\n<IMG SRC="lemma1.JPG" BORDER="0" ALT="">\n</CENTER>\n\n</HTML>\n\n!''Strong Live Event''\n<HTML>\nLive events allow us to express weak fairness constraints rather\nnaturally and it has been shown that both weak and strong fairness\nare expressible using live events. However, strong fairness\nconstraints may require more than what live events can offer in an\nintuitive way<A NAME="text1" HREF="#note1">1</A>.\n<CENTER>\n<IMG SRC="example5.JPG" BORDER="0" ALT="">\n</CENTER>\n\nIn general, construction like the above requires creation of\nadditional processes (for each strong fair associated event). For\ncomplex systems, a large of number of additional processes may be\nnecessary. Therefore, we introduce the notion of strong live\nevents (as a syntactic sugar) to capture strong fairness constraints\nelegantly. A strong live event is written as &#X113; (and\nevent &#XEA; is referred to as a weak live event). Let\n&#X3A3; be the set of all strong live events. If a strong live\nevent has been ready repeatedly, then it must be engaged\neventually.\n\n<CENTER>\n<IMG SRC="definition8.JPG" BORDER="0" ALT="">\n</CENTER>\n\n\nCompared to Definition 6, the additional constraint states that if a\nstrong live event is ready, either it becomes not\nready forever after some execution or it is eventually\nengaged. Note that the synchronization of an ordinary or weak live\nevent with a strong live event results in a strong one.\n\n<CENTER>\n<IMG SRC="example6.JPG" BORDER="0" ALT="">\n</CENTER>\n\nFor a process with only weak live events, its traces can be computed\nbased on the process expression itself (and the set of ready\nevents which depends on the process expression). The traces of a\nprocess with strong live events, however, depend not only on the\nprocess expression but also the history of the system evolution. The\nfollowing theorem shows the soundness.\n\n<CENTER>\n<IMG SRC="t1.JPG" BORDER="0" ALT="">\n</CENTER>\n\n\n\n<HR CLASS="footnoterule"><DL CLASS="thefootnotes"><DT CLASS="dt-thefootnotes">\n<A NAME="note1" HREF="#text1">1</A></DT><DD CLASS="dd-thefootnotes">In theory, strong fairness can be transformed\nto weak fairness at the cost of an auxiliary variable.\n</DD></DL>\n\n</HTML>

LTL - linear time temporal logic formulae for specifying correctness requirements. \n\nSYNTAX \n\nGrammar:\n ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl\n\nOperands (opd):\n true, false, and user-defined names starting with a ''lower-case letter''.\n\nUnary Operators (unop):\n [] (the temporal operator always)\n <> (the temporal operator eventually)\n ! (the boolean operator for negation)\n\nBinary Operators (binop):\n U (the temporal operator strong until)\n V (the dual of U): (p V q) means !(!p U !q))\n && (the boolean operator for logical and)\n || (the boolean operator for logical or)\n /\s (alternative form of &&)\n \s/ (alternative form of ||)\n -> (the boolean operator for logical implication)\n <-> (the boolean operator for logical equivalence)\n\nDESCRIPTION \nOur tool will translate LTL formulae into never claims automatically. So you do not need to write the negation for the property to be checked. The never claim that is generated encodes the Buchi acceptance conditions from the LTL formula. Formally, any omega-run that satisfies the LTL formula is guaranteed to correspond to an accepting run of the never claim. \n\nAll binary operators are left-associative. Parentheses can be used to override this default. Note that implication and equivalence are not temporal but logical operators. \n\nEXAMPLES \n[] p\n''!''( <> !q )\np U q\np U ([] (q U r))

This document presents the EBNF syntax of the specifica tion language used in our model checker. The name vCSP stands for variables enriched Communicating Sequential Processes. \n\n!''SYNTAX''\n\nSpecification ::= (Definition)+\nDefinition ::= Name ( Vars )? '=' ProcExpr ';'\nVars ::= Name ( ',' Name )* \nProcExpr ::= 'Stop'\n | 'Skip' \n | Event '->' ProcExpr \n | ProcExpr '[]' ProcExpr //-- external choice //\n | ProcExpr '<>' ProcExpr //-- internal choice //\n | ProcExpr '<' BoolExpr '>' ProcExpr //-- conditional //\n | ProcExpr '|>' ProcExpr //-- interrupt //\n | ProcExpr ';' ProcExpr //-- sequenctial componsition //\n | ProcExpr '|||' ProcExpr //-- (indexed) interleave //\n | ProcExpr '||' ProcExpr //-- (indexed) parallel //\n | Name -- //process reference //\n | (ProcExpr) \n\nEvent ::= Name | 'wl' '(' Name ')' | 'sl' '(' Name ')' \nName ::= ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'0'..'9'|'_'|'.')* ;\n\n!''OPERATOR PRECEDENCE''\nThe operators at the top of the table bind more tightly than those lower down. \n<html>\n<TABLE>\n<TR><TD>Class\n<TD>Operators\n<TD>Description\n<TD>Associativity\n\n<TR><TD COLSPAN=4><HR NOSHADE>\n<TR><TD>Sequential\n<TD><TT>-></TT>\n<TD>prefix\n<TD>right\n\n<TR><TD>\n<TD><TT>;</TT>\n<TD>sequence\n<TD>left\n\n<TR><TD COLSPAN=4><HR NOSHADE>\n<TR><TD>Choice\n<TD><TT>|&gt</TT>\n<TD>interrupt\n<TD>left\n\n<TR><TD>\n<TD><TT>[]</TT>\n<TD>external choice\n<TD>left\n\n<TR><TD>\n<TD><TT>&ltb&gt</TT>\n<TD>external choice\n<TD>left\n\n\n<TR><TD>\n<TD><TT>&lt&gt</TT>\n<TD>internal choice\n<TD>left\n\n<TR><TD COLSPAN=4><HR NOSHADE>\n<TR><TD>Parallel\n<TD><TT>||</TT>\n<TD>parallel\n<TD>left\n\n<TR><TD>\n<TD><TT>|||</TT>\n<TD>interleave\n<TD>left\n</TABLE>\n\n</html>\n\n!''EXAMPLES''\n\nThe spefication of two Dining Philoshpors:\n\nphi1()=((t1->phi1)[](wl(g1.0)->(g1.1->(wl(e1)->(p1.0->(p1.1->phi1)))))); \nf0()=((g0.0->(wl(p0.0)->f0))[](g1.0->(wl(p1.0)->f0))); \nphi0()=((t0->phi0)[](wl(g0.1)->(g0.0->(wl(e0)->(p0.1->(p0.0->phi0)))))); \nf1()=((g1.1->(wl(p1.1)->f1))[](g0.1->(wl(p0.1)->f1))); \nMain()=(phi0||f0||phi1||f1);

Critical system requirements like safety, liveness and fairness play important roles in system/software specification, verification and development. Intuitively, safety properties ensure that something `bad' never happens. Liveness properties state that something `good' must eventually happen, e.g., a submitted file must eventually be printed. Fairness properties state that if something is possible sufficiently often, then it\nmust eventually happen. Often, fairness assumptions are necessary to prove liveness properties. It has been proved that in some settings all properties can be decomposed into a safety property and a liveness property whose conjunction is the original.\n\nOver the last decades, safety specification has been studied extensively. There have been quite a number of specification languages and notations dedicated to safety-critical systems. For instance, there are state-based ones like Z, VDM, a variety of finite state machines and event-based ones like CCS and CSP. Liveness is as important as safety. A system satisfies a liveness property if and only if any finite run\ncan be extended to a run satisfying the liveness property. However, the concept of liveness itself is problematic, as commented by Lamport. Fairness constraints have proved to be an effective way of expressing liveness. Furthermore, fairness itself is important in system specification. A number of fairness constraints have been proposed and studied in automata theory based on accepting states, e.g., in the setting of Büchi/Rabin/Streett/Muller automata. Compared to safety, there are relatively few notations proposed for specifying liveness/fairness, especially in event-based systems, among which some have been evidenced.\n\nVerification of safety properties has been well studied. The common practice of verifying liveness relies on explicitly stating all fairness assumptions as premises of the liveness properties. If there are many fairness constraints, this approach may not be feasible. For instance, a standard method to prove that a program satisfies some property is Linear Temporal Logic (LTL) model checking. Given an LTL formula φ, the model checker transforms the negation of this formula into a Büchi automaton, builds the product of the automaton and the program and then checks this product for emptiness. The size of the constructed Büchi automaton is exponential in the length of φ. A formula composing of many fairness constraints results in a huge Büchi automaton and thus makes model checking\ninfeasible.\n\nIn this work, we propose an alternative approach for specifying and verifying systems with multiple fairness requirements. Instead of stating the fairness assumptions as a part of the property to verify, they are naturally embedded in the system (modelling) itself. We propose the notion of event-based fairness, i.e., a fairness constraint associated with individual events of the system. We show that by a syntactic language extension, a variety of fairness constraints can be specified intuitively. Next, we develop a model checking algorithm which takes the fairness constraints into account while building the state space. Experiment results show that our algorithm handles large numbers of fair constraints effectively.

[[Introduction]]\n[[Specification]]\n[[Event-based Fairness]]\n[[Software & Download]]\n[[Case Studies]]\n----\n[[About Us]]\n[img[email us|09.jpg][mailto:liuyang@comp.nus.edu.sg]]\n<html>\n<a href="/cgi-bin/pagecount?/~liuyang/veri/index.html">stats</a>\n</html>\n

<HTML>\n<HEAD>\n<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">\n</HEAD>\n<CENTER>\n<IMG SRC="pa.JPG" BORDER="0" ALT="">\n</CENTER>\n</HTML>\n

with tool support

Specifying and Verifying Fairness Enhanced Systems

Our tool is named Dike for the fairness execution of the processes. [[Dike|http://www.theoi.com/Ouranios/HoraDike.html]] (or Dicé) was the goddess of justice, fair judgements and the rights established by custom and law.\n\nCurrently, Dike 1.7 is available for [[download|http://www.comp.nus.edu.sg/~liuyang/veri/Dike.zip]] (see [[Version History]]). It has all functionalities as a complete model checkor for CSP (with fairness). We are still working on the improvements of basic editing functions as well as the model checking engine. Our aim is to develop an easy-to-user (compared with Spin or FDR), powerful and efficient model checking tools for process algebra.\n\n!''Features''\n*[[Complete Graphical User Interface]]. Much easier to use. No need to learn any commands and read any documentations (e.g. using spin). \n*Support Complete CSP language with Fairness Extensions.\n*Build-in LTL Pareser and Buchi Automata Converter. \n*Graphical Viewer for Convertered Buchi Automata.\n*Build-in Examples. [[Dining Philosophers]] and [[Peterson's Algorithm]]\n*Effecient Feasiblity Testing and LTL Property Verification.\n\n!''Screen Shots''\n[img[Dike|Dike.JPG]] [img[BAViewer|BAViewer.JPG]] \n\n!''Implementation''\nThe model checking tool is implmented using C# 2.0 and VS 2005. It has three important components list as follows:\n* Specification Parser and Recognizer. The parser is based on [[Antlr Parser Generator|http://www.antlr.org/]].\n* LTL to Buchi Automata Converter. This component is based on [[Paul Gastin's work|http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php]]. We also integrated the [[Graph Layout Execution Engine (GLEE)|http://research.microsoft.com/users/levnach/GLEEWebPage.htm]] by Microsoft.\n* Fast Model Checking Engine. The implementation is based on our proposed [[Algorithms]]. \n\n!''Installation''\nThe installation is pretty easy: upzip the file into a fold and click the executable Dike.exe.\nThe software is developed for Windows plantform. If you want to run it Linux, Solaris, Mac OS X, Windows and Unix, look at [[Mono|http://www.mono-project.com/Main_Page]]. \n\n!''Download''\nThe binary version of Dike 1.7 can be downloaded at [[Here|http://www.comp.nus.edu.sg/~liuyang/veri/Dike.zip]]. \nTo get the complete source code, feel free to [[contact us|mailto:liuyang@comp.nus.edu.sg]].\n\nSee [[Version History]] for the update changes\n\n\n!''User Manual''\n*[[How to write Process Definitions]]\n*[[How to write LTL Formulae]]\n\n

The fairness constraints studied in automata theory are associated with states. For instance, any execution of a Büchi automaton must visit at least one accepting state per fair set infinitely often. The notion of accepting states and its global constraints may not be directly applicable to event-based CSP/CCS or programs (which only captures safety properties). We believe that it is equally, if not more, important to have a notion of local (event-based) fairness to capture fairness/liveness constraints in event-based formalisms like process algebras or multi-threaded programming languages.\n\n!''Syntax''\nBecause concurrency is an important issue of process algebras, it is important for event-based fairness to cope with concurrent processes seamlessly. In the following, we introduce a core subset of Communicating Sequential Processes extended with shared variables and assignments.\n\n\n<HTML>\n<HEAD>\n<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">\n</HEAD>\n\n<CENTER>\n<IMG SRC="Syntax.JPG" BORDER="0" ALT="">\n</CENTER>\n\nProcess Stop does nothing but deadlocks. Process Skip terminates\nsuccessfully. Action prefixing a &#X2192; P is initially\nwilling to engage in action a and behaves as P afterward. An\naction is either an abstract event or an input (i.e., c?x) or an\noutput (i.e., c!v) or an assignment which updates the valuation of\nthe variables. Skip = &#X221A; &#X2192; Stop where &#X221A; is the\ntermination event. The sequential composition, P1; P2, behaves\nas P1 until its termination and then behaves as P2. A choice\nbetween two processes is denoted as P1 | P2. A choice depending\non the truth value of a Boolean expression is written as P1\n&#X25C1; b &#X25B7; P2. If b is true, the process\nbehaves as P1, otherwise P2. The state guard [b] @ P is\nblocked until b is true and then proceeds as P. Let &#X3A3;P be\nthe set of events appeared in P, i.e., its alphabet. Parallel\ncomposition of two processes is written as P1\n&#X2225; P2, where common events (&#X3A3;P1 &#X2229; &#X3A3;P2) of P1 and P2 are\nsynchronized. P1 &#X25B3; P2 behaves as P1 until the\nfirst event of P2 is engaged, then P1 is interrupted and P2\ntakes control. Recursion is allowed by process referencing. The\nsemantics of recursion is defined as Tarski&#X2019;s weakest fixed-point.\nTo make it more programming language like (and technically no more a\nprocess algebra), we assume that a system is composed of a set of\nprocesses and a set of global variables. The valuation of the\nvariables is a set of pairs, each of which maps a variable to its\ncurrent value (written as x &#X21A6; v). A specification is a pair\n(P, V) where P is a process and V is the initial valuation of\nthe data variables.\n\n<CENTER>\n<IMG SRC="example1.JPG" BORDER="0" ALT="">\n</CENTER>\n\nDespite its popularity and influence over quite a number of design\nlanguages such as Ada and occam, CSP lacks the notion of\nliveness or fairness. An event can be enabled forever but may\nnever be engaged. For instance, it is possible that agent3 never\ngets its turn to run even though the event update_nonshared is\nalways enabled. Furthermore, an event may be enabled\ninfinitely often but never been engaged. For instance, it is\npossible that one of the agents may greedily accessing the shared\nresource by repeating the sequence < request1, update1, release1\n> infinitely and thus leave event request2 enabled repeatedly in\nprocess Sem but never engaged. Such an infinite trace may not be\nfavored in a system designed with fairness assumptions in mind.\n</BODY></HTML>\n\n!''Semantics''\n<HTML>\n<HEAD>\n<META http-equiv="Content-Type" content="text/html; charset=US-ASCII">\n</HEAD>\nFor simplicity, we focus on the operational semantics in this paper.\nThe sets of behaviors of processes can equally and equivalently be\nextracted from the operational semantics, thanks to congruence\ntheorems. Fairness properties state that an event which is either\nrepeatedly or continuously enabled must eventually occur. They\ntherefore affect only the infinite, and not finite, traces of a\nprocess. We present an infinite trace semantics, inspired by the\ninfinite trace semantics for CSP. We remark that finite traces can\nbe naturally extended to infinite ones by assuming the specification\nis composed in parallel with a process that idles possibly\ninfinitely. Let &#X3A3; be the set of all events. Let &#X3A3;* be\nthe set of finite sequences of events. Let &#X3A3;&#X3C9; be the\nset of infinite sequence of events. &#X3A3;&#X221E; = &#X3A3;* &#X222A;\n&#X3A3;&#X3C9;.\n<CENTER>\n<IMG SRC="semantics.JPG" BORDER="0" ALT="">\n</CENTER>\nThe firing rules in Figure 1 are borrowed and extended from the ones\nin the operational semantics for CSP. Note that &#X3A3;P\nexcludes the internal action &#X3C4; and &#X221A;. Rule syn states\nthat two processes must not update the same variable at the same\ntime. This is guaranteed because only channel inputs/outputs or\nabstract events may be synchronized. We assume that assignments\nresult in unique events (ex&#X2032;:= g(x,y, &#X22EF;)) so that they are\nnever synchronized. All other rules are self-explanatory. An\ninfinite run of a process P with variable valuation V is an\nalternating infinite sequence of states and events (P0, V0), e0,\n&#X22EF; (Pi, Vi), ei, &#X22EF; such that P0 = P, V0 = V and\n(Pi, Vi) &#X21D2;ei (Pi+1, Vi+1) for all\ni. An infinite sequence of events is a trace if and only if there\nis a run with the exact same sequence of events. A state (Pj,\nVj) is reachable from (Pi, Vi) if and only if there is a\nfinite run from (Pi, Vi) to (Pj, Vj).\n<CENTER>\n<IMG SRC="figure1.JPG" WIDTH="782" HEIGHT="322" BORDER="0" ALT="">\n</CENTER>\n</HTML>

!''Version 1.7''\n02, Oct, 2007\nParser is re-implemented to support all possible definitions spefications.\nVerification can be done for user selectd Process definitions.\nLTL error message reporting function added.\nSyntax highlighting is added.\n\n!''Version 1.6''\n26, Sep, 2007\nMore meaning parsing error report for the specification is added.\nFull set of editing functions are added.\nThe tool is named Dike officially.\nLTL parser crashing is solved.\n\n!''Version 1.5''\n10, Sep, 2007\nComprehensive Multi-tab editing enviorments are integrated into the Dike.\nThe implementation is baesd on FireBall.\nLTL parsing options are added.\nPeterson's Algorithm Examples are added.\n\n!''Version 1.4''\n23, Auguest, 2007\nThe Buchi Automata Viewer is integrated.\nMC algorithms improved: Finite processes can be checked under fairness conditions\n\n!''Version 1.3''\n10, Auguest, 2007\nThe LTL to BA convertor is added.\nDinning Philosphers Examples are added.\n\n!''Version 1.2''\n2, Auguest, 2007\nThe parser of CSP is added, which is based on Antlr 3.0.\nGet All traces function is added.\n\n!''Version 1.1''\n25, July, 2007\nThe first implementation of the UI is finished.\nThe previous closure algorithm is improved for fast feasible and model checking.\nSeveral bug fixing for the model checking algorithms\n\n!''Version 1.0''\n3, July, 2007\nFirst implementation of the Dike.\nFeasiblity and Model checking algorithms is completed.\n\n\n