Home

MCMT v1.1.1 - User Manual (Draft)

1. 26 6 How to deal with In this section we give a couple of suggestions for formalizing some important subclasses of problems 6 1 Strictly sequential systems We call strictly sequential systems the array based systems in which all array variables are global These systems correspond for instance to programs manipulating pure arithmetical variables and no array at all We must say that MCMT is not structurally tailored to handle such problems and is far from being optimized for them however it can accept such specifi cations too In order to relatively improve its performances on such kind of problems it is better to avoid case distinctions at all when writing the update functions If all array variables are global MCMT models runs where N identical processes execute the same updates however if case distinctions in the update functions are abolished MCMT models runs where actually one process is working and the other ones are all crashed see the stopping failures model of Subsection 3 4 There is no real difference between the two models they are trivially bisimilar because all array variables are constant however the second model is computationally better behaved because adopting it MCMT does waste time in continuously adding the second quantified index variable and then realizing it was not needed In practice we suggest the following format for transitions in case all array variables have been declared to
2. UNIVERSITA DEGLI STUDI DI MILANO Dipartimento di Scienze dell Informazione MCMT v1 1 1 User Manual Silvio Ghilardi Silvio Ranise MCMT v1 1 1 User Manual Silvio Ghilardi and Silvio Ranise Dipartimento di Scienze dell Informazione Universit degli Studi di Milano Italy Fondazione Bruno Kessler Trento Italy December 20 2011 Abstract This document is addressed to MCMT users it explain from the beginning MCMT input specifications and illustrate some common settings and heuristics Advices for the formalization of some useful classes of examples are also supplied This is a draft subject to modifications and updates Contents 1 Introduction 2 Basic syntax A A AA 2 2 Index variables oc e e e we ee e ee 2 3 Array variables s so 2 44 ela a esca a a A 3 MCMT specifications 31 Initialization gender ee bo Se es Soe ee Pw See 3 2 Unsafe states aa a a a a a a a a a a 3 3 Transitions 3 4 Universal quantifiers in guards oo a a a e 3 5 System axioms LL 4 Running MCMT 4 1 Parsing Facilities sura pg e Ga AL Ae we Ae ee a we we aa 4 2 Options 4 3 Invariant search Options o oo a 4 4 Displayed information 5 Advanced Settings 5 1 Interaction 5 2 Bounded Resources in Invariant Search 5 3 Signature Abstracti0O 5 4 Quantifier elimination soe sema aa d e a n a a pa a e e a Da 5
3. executable mcmt It is strongly recommended to run the script mcmt_strict on input specification files whose syntactic correctedness has not been already certified memt can behave in an impredictible way if the input specification file is not correct In addition to the MCMT parser two options are supplied for debugging P activates a slow but rather accurate debugging procedure suitable formulae are generated and collected into a file named yices 1log this file is submitted through system calls to the type check Yices routine As soon as a parsing error is found MCMT tells the user where it is located and saves the related information into a file named p_error The option P requires the installation of Yices executable in the path of your shell Yices executable can be dowloaded from Yices website nttp yices csl sri com y produces an executable file for Yices named yices log if you have Yices installed you can run yices tc yices log to detect syntax errors from your input file that should be located in the strings to be passed to Yices 4 2 Options Each option has a short and an extended format which are equivalent We show here the short format type mcmt h to see both formats s disables most of the messages printed out by MCMT during the exploration of the search space of the array based system It only outputs the final statistics depth number of nodes number of calls to the SMT solver and number of
4. invariants found if any 16 b0 tells MCMT to apply a pure breadth first expansion of the tree nodes 4 According to the framework explained in 5 9 6 MCMT applies backward search by computing successive preimages of the unsafe configurations in this way it produces a search tree whose nodes are labelled by primitive differentiated formulae We call expansion of a node the operation of comuting its preimage i e the successors of the node itself in the search tree In the default setting MCMT first expands nodes labelled by primitive differentiated formulae with one then with two then with three variables etc With b0 option instead nodes are expanded in the same order in which they are produced b2 With this option nodes with n 1 variables are not only not expanded but not even produced at all before the tool has completed a full exploration of the nodes with n variables A further option b3 is available b1 gives the default setting this is the same as the b2 option but additional backward node subsumptions are tried pN gives the reader the opportunity of setting to N the increment in fix point tests fix point tests are incremental so as to reduce the size calls to Yices whenever inconsistency can be detected by analyzing just few initial nodes The default value is 3 wN enables an incomplete convex heuristics for fixpoint tests after N nodes expert use only f enables a flexible ins
5. just two variables respectively 14 System axioms can be used to specify conditions on the system topology e g that pro cesses are arranged as a partial order as a forest as a symmetric graph ete I or to specify invariants which are aready known to the user In case system axioms are not used to describe system topology or to express known invariants of the system they represent uni versal condition whatsoever imposed on the whole system i e invariants which are forced by the user This way of imposing constraints on traces is however not entierely appropriate because MCMT uses such constraints just in satisfiability tests and the formulae passing the tests are considered consistent as such in other words these formulae are not conjoined with the instances of the constraints used in the satisfiability tests themselves the consequence is that spurious unsafety traces might be occasionally produced REMARK in a system axiom there is no implicit assumption that the quantified variables x y jrepresent distinct indices so MCMT is allowed to identify them in instantiations this is different to the policy used for the format of primitive differentiated formulae transition guards and unsafe formulae where the variables z1 z2 are assumed to represent distinct indices REMARK it is not correct to use a system axiom to put a cardinality bound the sort INDEX see Subsection 5 6 for how to do this The reason is that MCMT u
6. process or to a channel To this aim we introduce a unary predicate P for being a process and leave the system axiom smt define P gt nat bool system axiom var x cnj P x S x T x to define it appropriately Another system axiom says that targets and sources are processes and not channels system_axiom var x cnj and P S x P T x A further system axiom might be used in case we want to ensure that channels having the same source and target are identical 22 Alternatively one could introduce two local arrays with values in the type nat and never update them in the transitions 28 system axiom Var x var y cnj gt and S x S y Tx Ty xy As claimed above this setting represents an approximation of 2 dimensional arrays which should be sufficient to address safety problems in specifications involving channels We expect that a future direct implementation of 2 dimensional arrays will produce considerable gain both in expressivity and in efficiency 29 References 1 P A Abdulla G Delzanno N B Henda and A Rezine Regular model checking without transducers In TACAS volume 4424 of LNCS pages 721 736 2007 2 P A Abdulla G Delzanno and A Rezine Parameterized verification of infinite state processes with global conditions In CAV volume 4590 of LNCS pages 145 157 2007 3 F Alberti S Ghilardi E Pagan
7. the trace could be spurious because of overapproximation Notice however that in some trivial cases Fourier Motzkin and integer quantifier elimination agree in such cases there is no overapproximation at all and no overapproximation warning is displayed Overapproximations of integer quantifier elimination are employed during invariant search too however no warning is displayed there because invariants are fully checked before being used in other words the overapproximation may cause the failure of the synthesis of some invariant but does not affect the correctedness of the final MCMT outcome 5 5 Acceleration MCMT supports a limited form of acceleration for single transitions not for sequences of transitions that could be useful for instance when analyzing Petri nets reachability If you write accelerate_transitionn k the system tries to accelerate the k th transition It will succeeds in case i the transition has an existentially quantified guard containing only one existentially quantified index variable that must be x according to our conventions from Subsection 8 3 11 only literals of the kind gt a x N and lt alx M where M N are integers and a is an array variable occur in the guard ii all local array variables a j are incremented decremented by a constant value in the x j case and left unchanged in the not j x cases iii all global variables are similarly incremented decremented I
8. val s j val w jl is the following exists x INDEX and alx 1 a s w lambda j INDEX case of Ex 2 s j w j and not x j s j 1 aljl s j w j and not x j not s j 1 8 s j w j where we indicated with a s w the updated arrays REMARK Version 1 1 gives the possibility of declaring transitions with zero variables in the guard this is particularly useful when formalizing time elapsing transitions in timed 12 systems To specify a zero variables transition just omit the var x declaration i e insert only the var j declaration before the guard Notice that in a zero variable transition the first case declaration of course is not reserved anymore to x j and universal quantifiers in the uguard see below are not anymore relativized to not x j 3 4 Universal quantifiers in guards It is often useful to have a limited form of universal quantification in the guards The kind of universal quantification we are considering leads to guards of the kind Ax olx A Yj plz 5 1 where Y are quantifier free formulae in only x occurs and in 4 both x and j can occur These guards lead outside the formalism of array based systems but there is a well known and good way of circumventing the problem The solution is that of adopting the so called stopping failures model in the stopping failures model processes can crash at any t
9. variables 25 5 9 Restricted Instantiation One of the key features of MCMT is full quantifier handling this requires full instantiation in the sense that quantified variables are instantiated in all possible ways during satisfiability tests instantiations are optimized by powerful but nevertheless complete heuristics Full instantiation prunes search space dramatically but can be expensive For this reason the user is given the possibility of limiting it especially in the final phases of the backward search computation Typing in the input file flex fix point fixed index var N flex_fix point_active_node_number M and using the option f from the command line the standard algorithm of MCMT is modified as follows After node M has been reached the first N variables are always instantiated iden tically in satisfiability tests for fixpoints If values for M N are not given in the specification file and the command line f is used MCMT employs the default values M 2 and N 50 5 10 Memory reset For difficult problems it empirically turns out to be useful to reset the SMT solver from time to time in order to prevent out of memory runs This is achieved by the following directives Directive Def Value Explanation start_reset N def N 375 after N nodes the SMT solver is periodically reset reset_ratio M def M 75 with ratio M intensive_reset P def P 30000 after P nodes the ratio becomes 1
10. want to check the universally quantified invariant Vz1Vz2C where C is a clause you must enter the literals corresponding to the negation of C The universal closures of the negations of the formulae you enter need not be inductive invariants MCMT will try by itself to complete them to inductive invariants e g if you enter a property which refers to a precise location MCMT will propagate it automatically to other locations if needed Hence the suggested negated_invariant block of instructions is particularly useful to insert code annotations in the specification files To this aim notice however that there is an alternative choice namely that of using multiple unsafe states descriptions see the u_cnj keyword Section 3 the two choices are declaratively but not procedurally equivalent In the case of suggested negated invariants MCMT tries to check the suggested invariants one after the other with bounded resources in case it does not succeed or it only partially succeed it will nevertheless proceed to the task of verifying the unreachability of the main unsafe configuration On the contrary in case of multiple unsafe states descriptions it will check unreachability of the declared unsafe configurations all together and will report unsafety in case at least one of them is reachable 21 5 2 Bounded Resources in Invariant Search When trying to check that a candidate invariant is indeed a true trace invariant MCMT has only boun
11. 5 Acceleration sos se ox ari e Ba we ga ed OO Sea a a Ba 5 6 Cardinality bounds a a 5 7 Key search 5 8 Variable redundancy ooa a 5 9 Restricted Instantiation 2 aa ee 5 10 Memory resetl 6 How to deal with 6 1 Strictly sequential systems 2 a a 6 2 Channels ao A A A O N N 14 16 16 16 18 19 21 21 22 22 23 24 25 25 25 26 26 27 27 28 1 Introduction MCMT is a model checker for testing reachability in a large class of formal systems called array based systems array based systems introduced in 5 comprise parametrized systems and sequential programs manipulating both arrays and arithmetical data This document is a brief guide on how to write input files and to run MCMT The input language is rather low level and input files in such a language should be auto matically generated from high level user interfaces or other verification tools However the knowledge of the low level input language is important for advanced use and for heuristics It should be noticed that MCMT performances even convergence might crucially depend on user defined settings and often these settings can be worked out only by slight editing of the MCMT specification files Roughly our language is composed of two sub languages one for describing a safety prob lem all keywords of this sub language starts with and one for describing conjunctions of literals to be passed to th
12. arrays is denoted by more precisely if zi is an index variable and a is an array variable identifier a zi is a valid term of the codomain type of a Similarly a x aly alj are valid terms too recall that x y j are the three special index variables These terms can be combined to form complex terms and literals according to the standard operation relations defined on the various types see the documentation on the Yices input language http yices csl sri com language shtml for more details For the sake of clarity if you like you can explicitly introduce a local array call it say i and think of it as the array of the identifiers in this way you can write lt i z1 1 22 instead of lt z1 z2 Notice that different processes must have different identifiers hence if you explicitly introduce the array of identifiers you must constrain it by a system axiom see Subsection explicitly stating this injectivity condition With the above declarations one can for instance write the following literals gt s z2 3 and w z1 v z4 true not alz1 2 s z1 z2 Other valid terms of tipes int and bool respectively are for instance s x 2 and or v y w jl the subtraction simbol must be used as a unary function symbol thus e g s x s y is illegal and s x 1 s y must be used instead Expressions like s 1 s 2 are not valid instead of the atom lt s 9 0 one must w
13. be global transition Var x var j guard lt list of literals gt numcases 1 case Val lt term 1 gt Val lt term 2 gt In addition we suggest to keep into consideration the possibility of indicating an abstract signature and of accelerating some transitions in order to avoid trivial divergency sources 27 6 2 Channels In many distributed system specifications communication channels arise in these specifica tions one can express for instance the fact that process p has sent an ack to process q by saying that ack is the location of the channel with source p and target q If it is implicitly assumed that there is a communication channel between any two processes whatsoever the most natural modeling of this setting would employ 2 dimensional arrays but unfortunately MCMT does not support 2 dimensional arrays in the present release We explain here the for malization we used in some examples of the distribution this formalization produces models which are slightly more general than the intended ones however they seem to behave properly in the applications The idea is that the type INDEX is reserved to channels channels have a source and a target and processes are identified with channels whose source and target coincide To get this it is sufficient to introduce two free function symbols smt define S gt nat nat smt define T gt nat nat We need to know whether an index variable refers to a
14. citly the literal not x j to the list of literals following the case keyword in other words the variable j always refers to a process different from x If the variables x y have been declared both the system assumes that they refers to distinct processes so you need not write not x y in the guard the guard is primitive differentiated by default However no specific case is reserved to the update of y if you want to make a distinguished update for y you must insert either y j or not y j in all the case distinctions except of course in the first one because not y x is assumed by default To summarize let us give an example The logical reading of 8In the term only the declared variables can occur i e we can have occurrences of x j and also of y in case the transition has two existentially quantified index variables The MCMT parser checks that and gives an error message if case of a numbering mismatch Notice that global arrays must be consistently updated in all the cases of the case distinction this is left to the user s responsibility mutually inconsistent updates would make the application of the transition inconsistent but MCMT can realize this only at runtime 11 transition var x var y Var a guard alx 1 numcases 3 case val 2 val s j val w j case s j 1 val alj val s j val w jl case not s jl 1 val 8
15. ction specifying the update of the transition e the cases specify through suitable conjunctions of literals the case partition used in the definition of the update function 10 e each keyword val is followed by a well formed Yices term of appropriate typef this term gives the updated value of corresponding array in the given case the number of val keywords must be equal to the number of array declarations thus if e g 5 local or global variables have been declared at the beginning of the file we must have 5 val lines for each case of the partition P The lt list of literals gt following the case keywords should represent all together a partition in the sense that the disjunction of such lists should be valid and all pairwise conjunctions should be inconsistent If the latter condition is violated MCMT works correctly but may do redundant work if the former condition does not hold MCMT implicitly adopts the stopping failures model see below and assumes all processes not satisfying any of the specified cases to get crashed The first occurrence of the case keyword must be followed by the single literal x j in case x j is omitted in the first case declaration the system automatically makes the correction this means in particular that the first case declaration can be followed by the empty list of literals in the specification files Similarly in the second third etc case the system always adds impli
16. d predicate symbols these symbols can be either free or constrained by system axioms see below to do that in the proper way just respect Yices input syntax The following line for instance smt define S gt nat nat bool defines a binary predicate S on natural numbers After this declarations literals like S 2 z2 not S z1 z2 3 will be valid 3 1 Initialization An array based system must be initialized In our specification files initialization is con strained by a universally quantified formula This is a compound command with the following format initial var lt indexvar id gt cnj lt list of quantifier free formulae gt There may be one or two occurrences of the keyword var lt indexvar id gt must be the special index variable x or the special index variable y The string lt list of quantifier free formulae gt is a finite list of quantifier free formulae intended conjunctively cf the keyword cnj where only the variables declared by var should occur although the parser in the current release of the system does not check this Such variables are implicitly universally quantified so for example the logical reading of initial var x cnj alx 1 s x false w x false is the formula in Yices format forall x INDEX and alx 1 s x false w x false 3 2 Unsafe states J formulae are obtained by prefixing a string 4z1 4zn of i
17. ded resources at its disposal This is because invariant synthesis can be ex pensive and can easily fail The user can modify these resources by specifying his preferred bounds in the input file these user defined bounds will be used in all the command line options involving invariant search namely i1 i2 i3 c a I as well as in the suggested _negated_invariant block of instructions above The following table summa rizes the directives about resource bounds in invariant search that can be introduced in the input MCMT specification files Directive Def Value Explanation inv_search_start N def N 0 begin invariant search after node N inv_search_max_index_var N def N 5 no more than N variables can arise in invariant search inv_search max num nodes N def N 150 no more than N nodes can arise in invariant search inv_search_max_num invariants N def N 200 find at most N invariants inv_search_max num_cand_invariants N def N 500 try at most N candidate invariants Notice that if the preassigned bounds are not sufficient search is interrupted and the candidate invariant is discarded The directive inv_search_only_candidates asks MCMT to generate candidate invariants without checking and hence without using them This can be useful in combination with the command line options dN e in shell scripts running many copies of MCMT in parallel 5 3 Si
18. e background SMT solver which is Yices Some familiarity with the theoretical framework of array based systems see the papers 8 6 5 9 7 could be useful though not indispensable when reading the rest of this document Remark The MCMT specification language has evolved and has been significantly simplified since the first beta version 0 1 Now the tool can get by itself some information previously required to the user nevertheless old fashioned files are still compatible with the new version and some files in the distribution might still contain actually redundant information Warning The parser of MCMT in its actual release should be able to catch the most frequent errors Since running the tool on syntactically incorrect files may cause an impre dictible behavior the reader is invited to read carefully the instructions in Subsection 4 1 below concerning the use of MCMT parser 2 Basic syntax The basic MCMT syntax include types index variables and array variables 2 1 Types Types that can be accepted by MCMT include nat int real bool i e natural integer real numbers and booleans New types can be declared by the user for instance the line smt define type locations subrange 1 8 declares the type locations consisting of 1 2 8 These finite interval types are partic ularly useful for defining program counter locations 2 2 Index variables A specification file for MCMT defines an array based sy
19. e of options that could be useful in such contexts but it is rather obvious that MCMT would need substantial enrichment to perform well on such problems First of all one can disactivate forward redundancy tests for formulae describing backward reachable sets of states by typing no_backward_simplification in the input file A much more useful option seems to be the possibility of classifying the formulae describing backward reachable sets of states whenever possible according to the value of a global variable This can be achieved by typing key_search g in the specification file here g should be a previously declared global array variable If the list of the formulae describing backward reachable sets of states is quite big this strategy alllows a more efficient access to that list during fixpoint tests 5 8 Variable redundancy Despite the fact that MCMT is quite optimized in this sense it is sometimes possible that redundant existential variables are produced during backward search such variables could be easily eliminated in case they have an explicit definition of the kind 32 2 tA MCMT can be forced to look for the possibility of such elimination by the directive variable redundancy_test Notice that this variable elimination procedure is always precise it does not cause overap proximations but may occasionally have undesired consequences on heuristics for invariant search especially in presence of global array
20. fied variables which can be either x or y The update function is a case defined function which is given in lambda abstraction notation the lambda abstracted variable must be j The format for a transition declaration is the following Tn order to avoid possible complaints by the MCMT parser please insert transitions after all initial unsafe system axioms and suggested invariants declarations 7 This is the format adopted in 6 and 9 the format of is more general however examples that can be formalized in the format of 5 can usually be formalized also in the 6 9 format if existentially quantified variables for data are allowed this topic will be covered in Section 5p 9 transition var x var y var J guard lt list of literals gt uguard lt list of literals gt uguard lt list of literals gt numcases lt pos int gt case x j val lt term1 1 gt val lt term1 2 gt case lt list of literals gt val lt term2 1 gt val lt term2 2 gt where e var y is optional it is needed only for two variables transitions while var x and var j are mandatory e the lt list of literals gt following guard is the lists of literals that forms the body of the guard of the transition e the lines starting with uguard are optional and will be discussed in the next subsection e lt pos int gt is a positive integer giving the number of cases of the case definable fun
21. found this means that the last displayed formula is consistent with the initial formula To get an assignment describing a state that can reach an unsafe configuration run Yices with the option e on the file yices log produced by the MCMT option y and take the last assignment displayed by Yices In case a spuriousness risk have been warned it is possible to check spuriousness of the trace but this can only be done manually in the present release of the tool 18Keep in mind that there might be a third case due to syntax errors in the strings forwarded to the SMT solver These can only be caused by syntax errors in the input file To avoid this misbehaviour use the script memt_strict see also Subsection 1 1 for debugging facilities 20 5 Advanced Settings In this section we explain some important settings of MCMT that can be obtained by includ ing special instructions in the input specification file sometimes such instructions must be combined with appropriate command line options 5 1 Interaction MCMT allows some form of interaction If you write in the input file suggested negated_invariants var zi var z2 cnj lt list of literals gt cnj lt list of literals gt end_of_suggested negated_invariants MCMT tries to prove the suggested invariants In case it succeeds it will use them later on in all consistency tests The lists of literals can contain at most the variables z1 z2 Notice that if you
22. gnature Abstraction Predicate abstraction is a powerful technique in model checking The current release of MCMT implements it only in an incomplete way we plan to have full abstract check refine cicles in CEGAR style in a future release What MCMT can do actually is to project during invariant search the candidate invariants it finds and their preimages over a subsignature indicated by the user This restricts the search and enhance the possibility of finding good invariants To specify the abstract signature type 22 abstract_signature subsignature k subsignature 1 subsignature m end_of_abstract_signature in the input file Here k 1 m are either 1 or 0 depending on the fact you want or you do not want the corresponding array to be abstracted away you have one line per array following the array variables declaration order Writing just dynamic_signature_abstraction you leave MCMT to find automatically the closest signature for abstraction when examining each candidate invariant Notice that all the above directives about signature abstraction are effective only when combined with the command line otions a I 5 4 Quantifier elimination To model real time systems in the timed automata style existentially quantified real integer variables may be used in guards You can introduce them in MCMT as follows First before writing any transition you must declare such variables as eevar lt char gt lt ty
23. i S Ranise and G P Rossi Universal guards rela tivization of quantifiers and failure models in model checking modulo theories To appear in Journal on Satisfiability Boolean Modeling and Computation JSAT Available at http homes dsi unimi it ghilardi allegati AGPRR_JSAT pdf 4 B B rard and L Fribourg Reachability Analysis of Timed Petri Nets Using Real Arithmetic In CONCUR 99 LNCS pages 178 193 1999 5 S Ghilardi E Nicolini S Ranise and D Zucchelli Towards SMT Model Checking of Array based Systems In Proc of IJCAR LNCS 2008 6 S Ghilardi and S Ranise Goal directed Invariant Synthesis for Model Checking Modulo Theories In TABLEAUX 09 LNCS 2009 7 S Ghilardi and S Ranise Model Checking Modulo Theory at work the intergration of Yices in MCMT In Proc of AFM 09 ACM Digital Library 2009 8 S Ghilardi and S Ranise Backward reachability of array based systems by SMT solving termination and invariant synthesis Logical Methods in Computer Science 6 4 2010 9 S Ghilardi S Ranise and T Valsecchi Light Weight SMT based Model Checking In Proc of AVOCS 07 08 ENTCS 2008 10 Nancy A Lynch Distributed Algorithms Morgan Kaufmann 1996 30
24. ime without any warning see 10 Adopting this model in our setting 9 basically means to introduce an extra crashed non crashed flag and an extra crashing transition the remaining transitions are modified so that crashed processes cannot be active in the guards and can never be repaired One can show that universal quantifiers in guards like can be removed if the stopping failures model is adopted Since all the above transformations are purely syntactic MCMT performs them automatically after informing the user that the stopping failures model has been adopted for details on these trasformations and their implementation in MCMT see 3 Notice that a safety proof for the stopping failures model implies a safety certification for the standard model too because the latter has fewer runs In case an unsafe trace is discovered however the trace might be spurious and MCMT displays a further warning in this sense Now we show how to insert universal quantifiers in the guards of the transitions of our specification files The formula y x j in can be rewritten as a disjunction of conjunctions of literals these conjunctions of literals can be introduced one after the other by using the keyword uguard There is an important limitation however the present version of MCMT does not support universal guards in case of transitions with two existentially quantified index variables otherwise said if you declare var y then you cannot use
25. les the use of x y but not of j is tolerated However you can never mix standard and special index variables in the same formula unsafe var zi var z2 cnj alz1 7 alz2 5 is the formula in Yices format exists z1 INDEX z2 INDEX and not z1 z2 alz1 7 alz21 5 If the set of unsafe states can be described by an 3 formula which is not primitive differ entiated it is possible to rewrite such 3 formula as a disjunction of primitive differentiated ones In such a case there is a special syntax for the second third etc disjuncts these can all be introduced by single commands u_cnj lt list of literals gt For these formulae there is no need of previous var declarations and the index variables z1 z2 z3 can be used without any numbering restriction but remind that MCMT cannot manipulate more than 10 index variables at all In case you use only u_cnj declarations and omit the unsafe formula i e if you omit the unsafe declaration MCMT works correctly it just adds false as a first unsafe formula 3 3 Transitions Transitions describe how a system evolves at each evolution step one transition is non deterministically chosen and executed if possible In an array based system transition are composed by a guard and an update funetion 7 The guard is an existentially quantified primitive differentiated formula MCMT accepts guards with at most two existentially quanti
26. lies transition 5 to za 23 then transition 6 to za etc when we say that transition 5 is applied to za 23 we mean that transition 5 has two exitentially quantified variables x y in its guard and that x is mapped to z2 whereas y is mapped to z3 Notation is rather informative but it is slightly incomplete because it does not mention which case in the case defined update functions applies to each variable displaying this information 19 too would result in a rather cumbersome outcome so in case of ambiguity it is necessary to consult the full information supplied by files produced by the options y r The remaining messages displayed by MCMT should be self explaining We just point out that MCMT supplies warnings for the only two cases where un unsafe outcome might be spurious e the stopping failure model has been adopted because of universal quantifiers in transi tion guards hence the unsafety trace can in principle be good for the stopping failures model but not good for the intended model e due to incomplete implementation quantifier elimination of integer data variables occur ring in the guards have been done imprecisely by overapproximating the set of backward reachable states In particular if neither universally quantified index variables see Subsection nor exis tentially quantified data variables see Subsection occur in the guards unsafety traces are not spurious In case an unsafe trace has been
27. n case it succeeds the original transition will be replaced by the accelerated one and the user will be informed about the success of the operation nothing will be said in case of failure Writing accelerate_all_transitions_you_can causes MCMT to try to accelerate all transitions but once again no sequence or cicle of transitions 2 The directive display_accelerated_transitions forces MCMT to print on the screen the accelerated transitions it finds 20The framework implemented in MCMT is roughly the same as that described in 4 21 To accelerate cicles the user must manually compute the composite transition of the cicle insert it as a further transition in the specification file and finally ask MCMT to accelerate it 24 5 6 Cardinality bounds If a parametrized problem looks too difficult one can try to verify it in special cases by imposing a cardinality bound on the sort INDEX This cannot be done by a system axiom by internal implementation reasons but there is the possibility of specifying such a bound in the input file by typing max_domain_cardinality N where N is a number like 3 4 5 etc do not use values greater or equal to 20 because the tool exits automatically when he realizes he needs more than 20 variables to solve the problem hence a value bigger than 20 would have no practical effect 5 7 Key search We made little experiments on using MCMT in planning problems It seems that there are a coupl
28. nd abstracted indexes are projected away this option may be combined with signature abstraction see Section 5 I same as i3 plus c plus a the latter with dynamic signature abstraction It is the most aggressive setting for invariant search it gives MCMT more chances to find useful invariants but at the same time it might considerably slow down the tool More information about invariant search will be supplied in Section 5 4 4 Displayed information If not run in silent mode MCMT displays some information about heuristics reachable states formulae trace invariants found and statistics We give here few explanations about node representation The meaning of the displayed line node19 t5_2_3 t6_2 t7_2 t6_1 t7_1 0 2 is that MCMT is considering a formula describing a set of states that can reach an unsafe state by executing transitions t5 t6 t7 t6 t7 in this order This formula is primitive differentiated and has three quantified variables that is it is of the kind 321 3223234 to see the formula you must inspect eit