The LTL Checker Plugins a (reference) manual
Contents
1. E Heuristics net diff partition p i Calculate fitness CONTINUO Calculate fitness STOP Sema Check correctness of EPC ILTL Checker Plugin 3 Default LTL Checker Plugin __ Plugin documentation Analysis LTL Checker Plugin Incorrect instances 920 Results 132f9n50 xm No mining action All Process Instances Results t32f9n50 xml No mining action Gelected Process Instances Figure 2 14 On the results the LTL Checker analysis can be done again also the using the LTL Checker plugin So it is possible to refine logs as far as you want till the point you are satisfied For example you can filter first all instances with property P and then on those instances check for property Q Of course you can create a formula R equivalent to P A Q which gives the same results but then you should know beforehand you want to check both P and Q Furthermore how smaller the log how faster the check 15 e Pro evvo File Analyse Convert Window Help Correct instances 7 using A Alpha algorithm plugin Incorrect instances 920 using Alpha algorithm plugin Correct instances 27 using Multi phase mining plugin Incorrect instances 920 using wo times D Multi phase mining plugin Correct instances 27 using prrect proce Genetic algorithm plugin Incorrect instances 920 using Genetic algorithm plugin Incorrect instances 920 using Tsi2. ee Normal Warning Error Debug Figure 2 1 The ProM window after a first start The LTL Template Import plugin is a plugin to import LTL Template files LTL Template files are files containing the specification of properties written in the special LTL Language Chapter 3 After importing such files the properties specified in it can be used to check workflow logs of processes which instances of the processes have the property The actual check is performed by one of the LTL Checker plugins The De fault LTL Checker plugin uses a standard LTL Template file with some common ltl properties defined in it By the normal LTL Checker plugin there is no standard LTL Template file you can choose which LTL Template file you want to use just import that one Both the Default and the normal LTL Checker plugins are analysis plugins These analysis plugins can be used on all mined logs given an appropriate input This means that if you will use the LTL Checker plugin you should first mine a log Fortunately there is an empty mining plugin in the framework using that mining algorithm mining is reduced to just reading the log In the next sections of this chapter all steps taken and windows encountered while using one of the LTL Checker plugins are explained in full detail The first plugin to be explained is the LTL Template Import plugin 2 2 Importing LTL Template Files The window of the
3. 2 010 Examples tst uw et ae SSS Aland in dr BE N s Parse Grrr nne we be Dn E esee ae RR RU RUM UST Propositional Logic ee 3 0 1 NOU 2 0 7 0 0227 AN zun oma al BA A A tiie REG eb ev AE 3088 WOL a oue uude e oem UE 2 0 4 Implication 4m m ate eee we ge tee RES 9 0 5 Bi implicati ni 2 team eg ASA A Ded 2 0 6 Examples u 4 4 ku Ivy R n Bi RUE do 367 Parse errors 4 2 a AA R e ae a e a 2200 4 03 35 37 Quantificational Logic 3 3 iss bh ombre dk i A 35 3 7 1 Universal Quantor 36 3 7 2 Existentional Quantor 36 3 069 Examples 2249994 a A AUS 36 Ji Parse eFTOES D xem in e xata a uae de aeo RW E S 3T 3 8 Linear Temporal Logic 37 3 9 L Nexte xs on amara do a abad sa Ll da Da 38 2 Eventually ande oe ea ar rr mA Rd en 38 O ALWAYS eb ore A A a 39 2 921 lan 1070007777 39 3 0 5 Examples e uae queden odeurs 78 A m e Roos 39 3 86 Parse errors 42 Grammar 43 Literals mde eR ee cen RN A A A A S 43 4 2 Identifier 3 Handtassen A A A dn d EL We 43 4 5 LTB Piles nt aan nea EAS EAS EEE A SS 43 4 Propositions az Socera aa Bo ak kek rein eene RR 44 Chapter 1 Introduction This document is both a user manual for the LTL Checker plugins of the ProM framework and a reference manual for the LTL Language If you are only interested in how to use t
4. A is done by person P A task P person lt h2 gt Does eventually P task A h2 lt p gt Is there a audit trail entry in a process instance in which person P does task A p lt p gt lt ul gt lt li gt lt b gt A lt b gt is a task of attribute lt i gt ate WorkflowModelElement lt i gt For this argument fill in the task you want to check for lt li gt lt li gt lt b gt P lt b gt is a person of attribute lt i gt ate Originator lt i gt Fill in the person you want to know if he or she perform task A li lt ul gt lt p gt j lt gt task A N person P formula does John drive Does John drive in a process instance eventually task A is done by person P driving John 27 Parse errors 3 5 Identifier is not a defined formula You try to use a identifier of a attribute or renaming as a formula and of course you can not call such a identifier as a formula Defined number of parameters not equal the number of arguments applied here You try to call a formula with not enough parameters or with to much parameters Of course this would not work so assure that the number of used parameters equals the number of defined arguments Identifier has not the right type You try to use a identifier of an attribute or renaming or a local one with a different type attribute than defined in the formula definition If at place x in the argument list a argument o
5. Again the figure of the running example now to explain the LTL operators 3 8 1 Nexttime The nexttime operator is a very basic and simple operator It express given a current audit trail entry something about the next audit trail entry in the sequence of audit trail entries in the current process instance So you can express more or less properties about subsequent states which have occurred The nexttime operator is an unary operator written as OC A In the Figure 3 5 where the current audit trail entry is D person Mary is true because in the next audit trail entry with name A the person is Mary If the current audit trail entry was not D but the C before it then 0 0 person Mary was true too You see the nexttime operator can be used repeatedly to express some property about a specific audit trail entry given the current Use this nexttime operator to express recursion about states T hen with the always operator see below you can check if a property A holds for all states of a process instance Remark that A never hold in the last state so to apply such recursion identify the last state so that always nexttime A holds or it is the last state Combined with a formula call you can use values of other states in the current comparisons For finalization it is recommended to use an end formula subformula Only in the last state holds that in the next state a WorkflowModelElement is not equal i
6. person Compute if person P is asking lt gt person P task asking formula moving or askingO All persons are either moving or asking around forall p person moving p C asking p 2 2 V C noving p N asking p 1 3 7 4 Parse errors e Identifier already in use in the local context You try to use a name for the dummy variable which is already used for something else e Identifier is not a defined attribute or renaming The attribute you want quantify over is not defined e Identifier has not type set The attribute you want quantify over is not a set 3 8 Linear Temporal Logic The LTL language elements are the logical elements which express properties about a sequence of audit trail entries of a process instance So an LTL property A is not a logical expression about the current audit trail entry but over the sequence of audit trail entries described by logic expressions about the current audit trail entry A and B are correct sub formulae as described earlier 37 05091 task asking person Mary date 1998 05 22 task 7 cycling task driving person John person John date 2038 12 02 date 2038 12 02 question Where am I distance 8 distance 103 54 answer Eindhoven y name Just a process instance case 234 Figure 3 5 Again the example process instance
7. 0 9 exponent 0 91 exponent exponent e E C 0 9 string literal 7 n rJ ON C n t b r f 2 20 desc literal z CTH CV Et br 7 5 10 2008 4 2 Identifier identifier 7 lt startletter gt letter digit lt startletter gt a z A Z letter a z A Z 7 digit 0 9 4 3 LTL File lt ltlfile gt 7 attribute lt renaming gt formulae attribute number string set attr name date cattr name date pattern date pattern 5 Xstring literal 43 attr name pi lt identifier gt lt renaming gt rename lt attr_name gt as identifier lt formulae gt formula subformula identifier arg list 5 z desc literal prop arg list arg lt arg gt lt arg gt identifier lt attr_name gt 4 4 Propositions lt prop gt lt unary_prop gt lt binary_prop gt lt quantification gt lt comparison gt lt formula_call gt lt unary_prop gt 212 LL 2 2 1 7 0 lt prop gt binary prop 2 2 prope 2 00 lt gt 2 U prop quantification forall exists identifier name prop
8. Defining attributes Ht set ate WorkflowModelElement set ate riginator date ate dob yyyy MM dd dates have the format year month day number ate distance string ate question string ate answer string pi name number pi case HH Renamings HH rename ate WorkflowModelElement as task rename ate riginator as person rename ate dob as bdate rename ate distance as distance rename ate question as question rename ate answer as answer 23 rename pi name as name rename pi case as case Parse errors e Identifier is already defined The new name is already in use as another renaming or formula name e Identifier is not a defined attribute You try to rename a formula or a renaming but that is not possible You can only rename attributes 3 3 4 Formula Definitions Now you can define attributes and rename them to something more writable you can use those definitions to define formulae There are two kinds of formulae formulae and sub formulae Both are defined exactly the same but the first keyword respectively formula and subformula is different The distinction is that sub formulae are not visible in the Template GUI Section 2 6 that is they can not be called by the user of the GUI Formulae are the visible formulae the formulae which the user can select and check A formula or subformula is defined as follows the keyword formula or subformula followed by an unique name a l
9. P person lt h2 gt Does eventually P task A h2 lt p gt Is there a audit trail entry in a process instance in which person P does task A lt p gt lt p gt lt ul gt lt li gt lt b gt A lt b gt is a task of attribute lt i gt ate WorkflowModelElement lt i gt For this argument fill in the task you want to check for lt li gt lt li gt lt b gt P lt b gt is a person of attribute lt i gt ate Originator lt i gt Fill in the person you want to know if he or she perform task A li lt ul gt lt p gt lt gt task A N person P Parse errors e Identifier already defined The name if this formula is already a defined identifier either of an at tribute a renaming or another sub formula e Identifier is already defined or used The identifier used as argument name is already used as argument name or as a global identifier that is of an attribute a renaming or a formulae e Identifier is not a defined attribute or renaming The identifier used as type of an argument is not a defined attribute or a renaming so it can not fulfill the role of an argument type 3 4 Formula calls A defined formula can be called in the actual formula part of a definition of another formula Important by calling a formulae is that the formula you want to call must already be defined you apply the right number of arguments and of course of the right type That is an argument of type A must be ap
10. The ProM framework EE E 2 complete Figure 2 6 The analyze menu to start the Default LTL Checker Plugin Now with this new window or another log activated so that it is the only active internal window of the ProM framework window you can run the Default LTL Checker plugin via the menu Analyze as is displayed in figure 2 6 After clicking one of the Default LTL Checker Plugin menu items a new window is opened the Template GUI Section 2 6 The Default LTL Checker plugin can also be started as you can the LTL Checker plugin but that is explained later Internally the standard LTL Template file is parsed This file called standard 1t1 and can be found in the lib plugins subdirectory of the ProM base directory You can change the contents of this file to your own needs But here again it is a good idea to try to parse a new standard Itl file before you use it Section 2 3 If the standard file can not be opened or parsed a message box is shown with the error message in it 2 5 Starting The LTL Checker Plugin While the Default LTL Checker Plugin does not need an imported LTL Template file the LTL Checker Plugin must have access to at least one such imported file Here too as was the case for the default plugin you should have an opened and mined log to use this plugin Once you have both log and LTL Template file you can start the LTL Checker Plugin by opening the Analysis window This plu
11. and the use of the formula is In the Template GUI see section 2 6 the contents of the 24 description are displayed in the description pane Because the description pane renders its content as HTML 3 2 you can use those HTML 3 2 tags to create a more elaborate description for the user In fact it is recommend to use HTML 3 2 code in your description But only the contents of the body tag should be used because the rest of the HTML code is supplied by the plugin itself Furthermore it is advisable to create your descriptions along the guidelines given below just to create a consistent view for the user On the other hand it is all up to you to do so or not I know programmers are lazy so empty descriptions shall be used much In principle there is nothing wrong with that as long as you are writing the formula definitions for your own But once you write your formulae for an unknown audience use the description wisely A description is made out of braces where in between the contents of the description are placed The guidelines for writing a description 1 Start with the title or name of the formula in between 22 tags 2 Divide your description into paragraphs using the p tags 3 In the first paragraph you give a short description of the meaning of the formula in terms of the arguments 4 in the next paragraph or in case of a simple formula in the first you list the arguments using an unordered list using the ul tag Ev
12. button and a new internal window is displayed the Template GUI 2 6 Using the Template GUI The ProM framework File Mine Analyse Convert Window Help simple log xml No mining action 4 E Results simple log xml No mining action Analysis Default LTL Checker Plugin Select formula Check options J eventually state A then E di eventually state A then B then C exists person doing task A and B exists person doing two different tasks Check till first success exists_state_done_two_times Check whole process Check till first failure person P does state A person P dot ate d Fur person P does state A and then B person P does state A and then eventually B vn the next time there is a state with name B Argurnents e A of type set ate WorkflowModelElement e B of type set ate WorkflowModelElement Valuate the parameters Name j set type a string B set type a string Figure 2 8 Choosing a formula in the Template GUI The Template GUI is a window consisting of four parts and a check button The first part is a list of formula names from which you can choose a formula This selected formula is used to check on the log Initially the first formula of the list is selected If no formulae are defined the item no formulae is visible and selected In the second part of the window the de
13. comparison attr name l lt gt 42 292 yei lt expr gt attr name in 212 string list string list 7 Xstring literal string literal formula call lt identifier gt param list param list 11 lt literal gt literal x literal 7 Xinteger literal real literal string literal lt expr gt 11 7 7 lt expr gt lt expr gt 24 I3 2 ip lt expr gt 2 literal attr name 44 Index Comparisons 28 Examples 31 Parse errors 32 Defining attributes Date 21 Examples 22 Number 20 Parse errors 22 Set 21 String 21 Error Comments 20 Comparisons 32 Defining attributes 22 Formula calls 28 Formula definitions 26 LTL 42 Propositional logic 35 Quantification 37 Renamings 24 Examples Comments 20 Comparisons 31 Defining Attributes 22 Description 19 Formula calls 27 Formula definitions 25 LTL 39 Propositional logic 35 Quantification 36 Renamings 23 Exporting in the ProM framework 14 Formula call 26 Examples 27 Parse errors 28 Formulae 24 Description 24 Examples 25 List of arguments 24 Parse errors 26 Grammar 43 Identifier 43 Literal 43 LTL File 43 Propositions 44 Importing in the ProM framework LTL Template files 5 Importing LTL Template files 5 LTL 37 Always 39 Eventually 38 Examples 39 Ne
14. data elements containing date strings Because there are many forms in which a date can be described a special string the date pattern is added to the date type attribute definition The date pattern is afterwards used to cre ate a SimpleDateFormat object of the Java programming language The format of date patterns allowed is described at http java sun com j2se 1 4 2 docs api java text SimpleDateFormat html a web page containing information about the SimpleDateFormat class For now we give a short description on how to create a date pattern for a full explanation read the web page mentioned earlier In short a date pattern exists of characters with special meaning If you want to put characters themselves in a data pattern use a to enclose them Now a table with some date characters are given This list is not complete therefor again have a look at the web site mentioned earlier year month in year week in year week in month day in year day in month day in week hour in day 0 23 hour in day 1 23 minute in hour second in minute millisecond MX earthed eX 21 With these date characters you now can build date patterns like yyyy MM dd thus strings of the form 2006 12 09 date ddMMyy strings like date 230907 HH mm strings denoting time like 12 45 You define a date attribute for data element data element and date pattern date pattern as follows date pi data element da
15. of today formatted in the format specified by the definition of the attribute for both string and set attribute parameters the initial value is type a string You can only fill in those values that are acceptable values for the different kinds of attribute types This means that every value in case its type is number or date is parsed to a value of that type If this parsing is successful the new value is placed into the table if the parsing does not succeed the old value does not change It is good to know that you can only fill in literals That is attribute names string lists and other formulae are not accepted as values they are interpreted as strings and in cases of date and number attributes they are parsed as dates or numbers respectively Once you have set the values you want for the parameters you can use the next part of the Template GUI to set some check options This part is right of the list with formulae There are three options you can choose from 1 Check whole process Check all process instances in the log for the selected formula 2 Check till first failure Check all process instances in the log but stop at the first encountered process instance not having the property specified by the selected formula 3 Check till first success The reverse of the previous item Check all process instances in the log but stop at the first encountered process instance having the property 11 GO File Mine Analyse Conve
16. results in true for all task other than asking and for those task equal to asking with a non empty answer task asking gt answer subformula distance between lbound distance ubound distance The distance of the current audit trail entry lies between the lower bound and the upper bound distance gt lbound distance lt ubound subformula reasonable distance If the task is cycling the distance must be between 0 and 65 if the task is driving is must be between 0 and 300 if the task is flying the distance must be between 150 and 1340 JA task cycling gt distance betveen 0 65 task driving gt distance between 0 300 AS task flying gt distance between 150 1340 subformula permitted to drive A person is permitted to drive if he or she is born before 2004 6 01 bdate 2004 06 01 subformula a important case Case is important if the word important important x is used in the name name task B task not equal to B p subformula P does A A not B P person 4 Compute if person P does task A which is lt gt task A N task B person formula exists person doing two different tasks Is there a person doing two different tasks exists p person exists t task exists u task P does A A not B p t u N P does A A not B p u t m
17. ProM framework will look like the window displayed in Figure 2 1 In this figure the window of ProM is displayed directly after starting ProM While using ProM thus after mining importing and analyzing this window may be filled with many internal windows Because the goal of this chapter is to teach you how to use the LTL Checker plugins it is assumed that you start ProM from scratch just to keep things simple File Mine Analyse Convert Window Help Open b MN Analyse Ro Convert Import D HN file Export ETE template file Recent files gt PNML file Exit TPN file Aris graph format Figure 2 2 The import menu For importing an LTL Template File you go to the File menu and then to the sub menu Import In this menu you can choose one of the items listed Figure 2 2 one of items is LTL template file Click on this item and a new open dialog is displayed m Mine Analyse Convert Window Help Look In TemplateFiles M 63 dates tu E Rws iu Ey testiu 3 test2 1u File Name ranges Itl Files of Type LTL files 1th M Open l Cancel Figure 2 3 The open dialog for importing LTL Template files In this dialog you navigate to the directory containing the LTL Template file you want to import select this file and click the Open button Figure 2 3 It is a good custom to give your LTL Template f
18. Section 3 6 those logical operators are used although the meaning may not be completely clear yet 1 version 0 5 This part of the file is as in example version 0 4 uu subformula has AnswerO If the task is asking then there is a answer not equal to the empty string This formula results in true for all task other than asking and for those task equal to asking with a non empty answer task asking gt answer subformula distance between lbound distance ubound distance The distance of the current audit trail entry lies between the lower bound and the upper bound distance gt lbound distance lt ubound subformula reasonable distance If the task is cycling the distance must be between 0 and 65 if the task is driving is must be between 0 and 300 if the task is flying the distance must be between 150 and 1340 task cycling gt distance between 0 65 A task driving gt distance between 0 300 A task flying gt distance_between 150 1340 subformula permitted to drive A person is permitted to drive if he or she is born before 2004 6 01 bdate 2004 06 01 subformula a important case 4 Case is important if the word important is used in the name name important 3 5 7 Parse errors e ldentif
19. The LTL Checker Plugins a reference manual HT de Beer H T d Beer student tue nl Eindhoven October 3 2005 Contents 2 1 2 2 2 3 2 4 2 5 2 6 221 2 8 2 9 3 1 3 2 3 3 3 4 3 5 3 6 Introduction Use of the LTL Checker Plugins Introduetion ERR e ene RISE ere ta Importing LTL Template Files Using the stand alone LTL Parser Starting the Default LTL Checker Plugin Starting The LTL Checker Plugin Using the Template G 1 Viewing the Results Exporting the Results Reusing the results raped d ela ala ae azal ali ae oe aerden f LTL Language Introduction sa se iaa ka EEE e The Environment in which the Language operates 3 2 1 A running Example Definitions and Comments 2 92 Comments m Da e 3 3 2 Attribute Definitions 3 3 3 Renaming of defined Attributes 3 3 4 Formula Definitions Formula call uk co aoe sz ee l l add EAS 5 6 Comparisons sexos RG ERO e 79 a 9 4 RASA AUS 3 5 1 Standard comparisons 3 5 2 The string type operators and literals 3 5 3 The set type operators and literals 3 5 4 The date type literals 3 5 5 The number type literals and expressions
20. ary date 1998 05 22 task 7 cycling task driving person John person John date 2038 12 02 date 2038 12 02 question Where am I distance 8 distance 103 54 answer Eindhoven NS name Just a process instance case 234 Figure 3 3 Again the example process instance A comparison exists of a left hand side attribute thus no local argument with an operator and a right hand value This right hand value is either a literal an attribute or renaming or local argument or a more complex expression in case of number attributes A comparison results always false if in the current audit trail entry the left hand side attribute and thus a eventually right hand side attribute too does not exist In the running example a comparison of the form answer results in false because the current audit trail entry D has no answer data element So if you use a data element which does not exist for all audit trail entries be aware of the strange or unexpected results formulae may result 3 5 1 Standard comparisons The first standard comparison is the well known equivalence or is equal op erator It compares the left hand side with the right hand side Of course it is true when both sides results in the same value given the current audit trail entry and process instance In the example situation of Figure 3 3 where the audit trail entry labeled D is the curr
21. d with the LTL operators but can with the quantors and vice versa On the other hand there is a drawback by using quantification it is very costly because quantification over a set S with property A results in a property of length S times the length of A So it is advisable to try to use the LTL operators in stead of the quantors when possible But as said before quantification is sometimes needed mostly to say something about all elements of a set If one wants to ask about one specific instance of a set use the LTL operators 35 The standard data elements of an audit trail entry WorkflowModelElement Event Type and Originator are the most likely candidates for quantification and thus for being a set attribute But all data elements can be sets and therefor used for quantification so Timestamp or distance too But then those attributes are sets and the value of the element is a string rather than a date or a number 3 7 1 Universal Quantor The universal quantification computes if a property A holds for every element in a set S That is the property Vses As An universal quantification is written as follows forall i SetAttribute A 1 With i SetAttribute a local renaming i for attribute Set Attribute of type set The property to check for all iis then A If A holds for all i this quantification is true 3 7 2 Existentional Quantor The existentional quantification computes if a property A holds for any element in a s
22. e line before renamings and so on Later on in this chapter you will see examples of this Parse errors No errors specified 3 3 2 Attribute Definitions Definitions of an attribute are more complex than writing comments but it is easy enough An attribute definition starts with a keyword denoting the type of the attribute There are four types and thus four keywords number set string and date After the type you give the name of the attribute This name must be unique and exists of two parts a scope prefix and the name of the corresponding data element in the workflow log The scope prefix is either ate or pi and denotes if the data element is an element of an audit trail entry ate or if the data element is an element of a process instance pi So if a data element exists as well as a process instance element and as an audit trail entry element you can define both as an apart attribute because the scope prefix results in two different names If you are not defining a date attribute you are ready after putting a semi colon For a date attribute you should give the keyword followed by a date pattern and finally a semicolon too Hereafter the different types are described e number The first type of attribute you can define is the number attribute A num ber attribute can contain values that can be parsed as integers or floating point numbers internally both integers and floating point numbers are parsed to floating p
23. e of birth is lesser or equal to the previous one Hereby the end formula is needed to finalize the formula that is that the property holds in the last state subformula next older d bdate Is d bigger or equal the current date 0 bdate lt d formula always nexttime olderO Holds always that the birth date of the person in he next audit trail entry is lesser or equal to the date of birth of the person performing the current audit trail entry C C next older bdate end 3 8 4 Until The until operator is the most complex operator but it states that A holds till B holds When B holds A may hold as well You express this as A UB Remark that if B never hold but A does always from the current audit trail entry the property is true As example a property expressing that until there is any distance moved only questions are asked formula move till questionO task asking _U distance gt 0 3 8 5 Examples This section already contain useful examples so here the last and complete version of the ltl file is given to conclude this chapter This example file can also be found together with this manual in a file named running ltl A test log is also supplied with name running xml version 1 0 39 date 01122004 b author HT de Beer HH HH Defining attributes HH set ate Wo
24. e you can construct more elab orate regular expressions and more operators are available To conclude this very short introduction on regular expressions some examples 30 word Search for strings with word in it like this sentence ID 0 9H 5 5 Search for strings starting with ID and followed by five digits ID98324 ID12347 etc a b Search for sequences of n a s followed by m b s like aabb abbbbbbbb aaaaaaaabbbb etc yes Yes y Y Search for different ways to express yes 3 5 3 The set type operators and literals The set literals are exactly the same as string literals That is easy explained the sets exists of just strings Furthermore the standard operators can be seen as a cast to strings before using them so you can test an individual value of the set to another value Sets are used for quantification and therefor it is an apart type Nevertheless a special set operator is defined the in operator It tests if the left hand side attribute is in a by the user given set It is of the form attribute the in keyword and a list of strings separated by comma s between and l Because the language does not enforce the list to test for duplicates in the set it can be a multiset or bag too In fact internally it is transformed to a set but for you as user of the in operator it is a bag In the running example a expression could be person in John Mary Angilbert that is test whether the per
25. ed attribute 22 3 3 3 Renaming of defined Attributes A renaming is exactly what it says a renaming In this case you can rename a defined attribute which must be the name of the data element prefixed with either pi or ate to a shorter more readable or understandable alternative In fact you can define as many alternatives as you want as long as every alternative has an unique name Of course as is usual in programming languages a name can not be equal to one of the keywords Thus as ate date exists forall formula in number pi rename set string subformula are not permitted as names for renamings and formulae Furthermore a name starts with a letter and can consists of letters digits and A renaming can be created by the keyword rename followed by the attribute name the keyword as the new name and finally the semicolon as is the case for all definitions Thus for attribute name old name and new name neu name you write a renaming as follows rename old name as new name Examples We now adapt our running example so that the defined attributes are named as in figure 3 2 So ate WorkflowModelElement is renamed as task ate Originator as person and ate dob as bdate For the other attributes we rename them to a new name without the scope prefix version 0 2 date 01122004 author HT de Beer HH
26. ent audit trail entry a comparison like task driving would result in true because task referring to the ate WorkflowModelElement and corresponding data element has in the log the value driving Ifthe comparison was task asking it would result in false because the data element WorkflowModelElement of the current audit trail entry has value driving The is not equal operator A B is equal to A B Subsubsection 3 6 1 and is the reverse of the operator So in the running example where D is the current audit trail entry task asking is now true and task 1 driving false lt The lesser than or equal operator is denoted as lt and does just what you expect that it does Especially for date and number attributes this operator 29 and the counterparts gt and gt are useful For string and set attributes you can use them for properties about the alfa numerical ordering of strings In the example distance lt 200 results in true in the current audit trail entry there the distance is equal to 103 54 gt The bigger than or equal operator is denoted as gt and does just what you expect as all the standard operators do lt The lesser than operator is denoted as lt gt The bigger than is denoted as gt 3 5 2 The string type operators and literals A string literal looks like most string literals in most programming languages two quotes in which between the con
27. error There are three kinds of errors possible 1 Error occurred during parsing The file is opened but the contents are not parseble by the LTL Parser The most likely reason is that you have made an error by writing ltl expressions 2 Error while reading filename Check the file name and try again There are problems with opening and reading the file Maybe the file does not exist or it is already in use by another program 3 Unknown error All errors not of kind one or two are unknown that is they are not expected by the parser but are thrown nonetheless Most likely it is then a bug so send a bug report containing the error message and LTL Template file you try to import 2 4 Starting the Default LTL Checker Plugin The ProM framework File Mine Analyse Convert Window Help 371 372 Show Process Instance Originator Figure 2 5 A log is mined with the No mining action mining plugin How to start the Default LTL Checker plugin is explained in this section The Default LTL Checker Plugin can be started on every mined log that is the active internal window of the ProM framework window should contain such log For now we open just a log an mine it with the No mining action mining algorithm Figure 2 5 This mining plugin does nothing but read the log and displays the contents of it in a new window If you want you can visualize one process instance
28. ery item in the list create a list item with the li tag starts with the name of the argument in bold 9 tag followed by the meaning of the argument Give then the attribute in italics tag and the type of the attribute eventually in italics too Then a recommendation of the value the user should give For example a range or the pattern of the date pattern in case of a date attribute 5 Write now a more detailed description and or other remarks if needed The actual formula The actual formula is given in terms of propositional logic section 3 6 quantifi cation section 3 7 linear temporal logic Section 3 8 comparisons Section 3 5 or sub formula calls Section 3 4 That is the actual formula consists of correct expressions in this language combined to bigger expressions by the operators in this language Examples For the running example we define now one formula in which you see all ele ments of a formula definition Because till now you have not learned how to write the actual formula a very simple formula is defined The description as is given here is the only full description according to the guidelines you will read in this manual because the goal is to learn to write ltl formulae not to write good descriptions 25 HERRERA HAAR b version 0 3 Poara This part of the file is as in example version 0 2 dris Formulae HH formula eventually_task_A_is_done_by_person_P A task
29. ess can be seen as a list of N process instances Every process instance itself is a list of M ordered audit trail entries Figure 3 1 Actual M can be different for any process instance Both audit trail entries and process instances can have data fields About audit trail entries we know that there are always a WorkflowModelElement and an Event Type data field other fields are permitted too 17 N process instances M audit trail entries per process instance Figure 3 1 A log In the language those date fields can be accessed by defining Subsection 3 3 2 attributes of the appropriate type number set string or date for the data fields Later these attributes can be used in logical expressions via comparisons Section 3 5 The value of these attributes depends on the current audit trail entry while checking the log A log is checked one process instance a time Every process instance is checked by inspecting the audit trail entries one for one from the last till the first The current audit trail entry is that audit trail entry which is currently inspected by the checking algorithm The value of an attribute is computed by getting the value of the corre sponding data field of the current audit trail entry If needed this string value is parsed to the appropriate type thus in case the attribute is defined of type number or type date it is parsed In the language you can use different sorts of logical express
30. et S That is the property Ises As An existentional quantification is written as follows exists i SetAttribute A 1 With i SetAttribute a local renaming i for attribute SetAttribute of type set The property to check for all iis then A If A holds for any i this quantification is true 3 7 3 Examples In the running example are now more complex properties specified using quan tification For example a formula to test if there is a person doing two different tasks The universal quantification is used to specify the property that all per sons doing either moving or asking around not both Both properties are about one process instance and that for all process instances b version 0 6 55 This part of the file is as in example version 0 5 Hone subformula P does A A not B P person A task B task 1 Compute if person P does task A which is not equal to lt gt task A N task B N person P formula exists person doing two different tasks Is there a person doing two different tasks exists p person exists t task exists u task P does A A not B p t u N P does A A not B p u t 36 subformula moving P person Compute if person P is moving person P N task driving M task cycling task flying subformula asking P
31. f type A is defined use a value of type A on place x in the parameter list of the formula call Identifier is not a local parameter in this contest You try to call the formula with a identifier that is unknown in the local context so it is not known as a defined attribute or renaming and not as a argument to the formula in which the call is written down Unable to parse this as a date given definition xyz You fill in a date string as parameter but this string can not be parsed according to the definition of the used attribute in the argument list of the formula definition Type mismatch You try to use a string value on an argument of attribute with type num ber Not expecting a integer A integer is applied where no number is expected Not expected a floating point number A floating point number is applied where no number is expected Comparisons The basis of formula definitions are the comparisons that is the comparisons of attributes and thus data elements of process instances of audit trail entries with other values which may be attributes too but literals are also possible All attribute types have a number of standard comparisons common and some have their own extra comparisons First are the standard ones explained then per type the literals and special comparison operators are described But before that the common form of a comparison is given 28 05091 task asking person M
32. gin can not be ac cessed through the Analyses menu because it needs two inputs a log and an LTL Template file it is up to you to select the appropriate input G The ProM framework File Mine Analyse Convert Window Help and Perform analysis L7 ee ee s ee Petri net Analysis Workflow log of a process Eno Replay Analysis Results t32f9n50 xml No mining action All Process Instances Heuristics net diff union Heuristics net diff partition Parsed LTL file Calculate fitness CONTINUO Imported standard lti LTL template file TL Parser v Calculate fitness STOP Imported standard ltl LTL template file TL P Check correctness of EPC LTL Checker Plugin q Default LTL Checker Plugin Plugin documentation Parse Figure 2 7 The analyze window You can open the Analyze window by clicking on the binoculars button on the toolbar or press ALT A This window is displayed in Figure 2 7 As you can see on the left hand side of the window you can select an analyze plugin In this case you will select the LTL Checker Plugin But as said before you can also select the Default LTL Checker plugin On the right hand side of the window you can select the log to check the first combo box and the imported LTL Template file in which the property to check can be found Now the LTL Checker Plugin has enough information to start so click the Nezt
33. he plugins just read Chapter 2 In that chapter you will read about how to import your own LTL Template files via the LTL Template Import plugin Hereafter the most attention is on how to start and use the Default LTL Checker plugin and the normal LTL Checker plugin At the end of the chapter you will see that results obtained from using the LTL Checker plugins can be used again in the ProM framework as you can use every log On the other hand if you are interested in how to specify your own LTL properties you will have to read chapter 3 too That chapter explores all the details of the LTL Language from defining attributes to creating complex LTL expressions This chapter uses a simple running example to explain all the language elements This example is as LTL Template file and test log file added to this manual running 1tl and running xml The last chapter contains the grammar of the LTL Language It can be used as a short summary of the chapter about the LTL Language without any explanation the structure of the language is presented Chapter 2 How to use the LTL Checker Plugins 2 1 Introduction This chapter is about how to use the LTL Checker plugins There are three different plugins which are all grouped under the name LTL Checker plugins These plugins are an LTL Template Import plugin a Default LTL Checker plugin and the normal LTL Checker plugin The ProM framework 000 File Mine Analyse Convert Window Help
34. ier is not of type string This error is shown if you try to use the regular expression operator on attributes not of type string e ldentifier is not of type set This error is shown if you try the in operator with attributes not of type set e Expected value of type number 32 You have used the special numerical operators with values or attributes which are more or less values too not of type number e Unable to parse this as a date given definition Shown when you specify a date literal which is not parseble with the pattern specified by the associated left hand side date attribute e Expected a string You use a left hand side attribute of type string but the value you specified can not be parsed as such e Identifier not defined You try to use an attribute or renaming as a value which is not defined before use hence this error e Type mismatch The left hand side attribute and right hand side value does not match types 3 6 Propositional Logic Now the comparisons and literals are explained the basis for the propositional logic is laid because the atoms of the propositional logic in the LTL language are those comparisons Furthermore properly defined formulae exists of atoms too so they can be seen themselves as behaving like atoms that is resulting in true or false Let A and B correct atoms or formulae They are used to combine DE 8 them with logical operators to larger e
35. iles the extension because you will more easily recognize your ltl files and in the open dialog files are initially filtered on this extension The ProM framework File Mine Analyse Convert Window Help 7 Imported standard it LTL template file formula exists state done two timesQ h2 gt Does a state exists which is done two times after each other h2 gt p Is there a state which is done and in the next state too lt p gt exists s state eventually state A then B s s 1 formula exists person doing task A and B A state B state 412215 there a person doing task A and B lt h2 gt p ul li b A b of type set lt i gt ate WorkflowModelElement lt Ji li li b B b of type set lt i gt ate WorkflowModelElement lt i li Jul lt p gt exists p person person P does state A p A X person P does state A p B J subformula not_eg A state B state l state state B subformula P does A A not B P person A state B state Figure 2 4 The contents of the imported LTL Template file are displayed Now the framework tries to open the LTL Template file The file is parsed by the LTL Parser and the contents of the file are putted in a read only text box This window you see it on Figure 2 4 has no functionality at all but may be in some future it will become
36. ing Example In this chapter a running example of a log existing of process instances of persons doing different tasks is used Every process instance has two data fields a name and a case number For every audit trail entry minimal three data fields are available WorkflowModelElement here called task Originator here called not mentioned any more task asking person Mary person John person John date 1998 05 22 person and Timestamp here not used Furthermore all audit trail entries do date 2038 12 02 date 2038 12 02 question Where am I have a EventType data field but the value is always complete so this field is task 7 cycling task driving distance 8 distance 103 54 answer Eindhoven name Just a process instance case 234 Figure 3 2 An example process instance Besides those standard data fields audit trail entries can have extra data fields depending on the task In Figure 3 2 you see a visualization of one of such process instances of the example log On the figure you see the current process instance that is the process instance for which a property is computed The current audit trail entry is the one with the red circle or the grey circle called D When new language elements are introduced they are explained by using this figure To be complete for this running example there are two files added to the manual
37. ions First of all the normal propositional logic This logic is about truth values only that is an expression is true if the operator applied on the operands results in true otherwise it results false The context of a propositional logic expression is determined by the temporal operators If no temporal operators are used a logical expression is about the first audit trail entry of a process instance only Another sort of logic is the quantificational logic which you can use to specify properties over all members of a set Here again the context of a quantificational expression is determined by temporal operators The last kind of logical expressions are linear temporal logic expressions With these LTL operators you can specify properties about the current audit trail entry the next current trail entry given the current audit trail entry any audit trail entry given the current or all audit trail entries given the current audit trail entry The current audit trail entry is initial the first so by not using temporal operators all logical expressions are about this first current initial audit trail entry The temporal operators are the operators which gives you the possibility to specify properties about a whole process instance about all audit trail entries of a process instance You can specify temporal relations between audit trail entries and so you change the context of the normal logical expressions 18 3 2 1 A runn
38. ist of parameters between paren theses the list may be empty the keyword a description the actual for mula and finally the well known semicolon Thus formula A formula name argi attri arg2 attr2 A description actual formula doing something with the arguments The different elements of a formula definition are now explained The list of arguments of a formula The list of arguments is a comma separated list of so called local renamings that is a new unique name in the local context followed by a colon and the attribute the new name is a local renaming for The name of the local renaming can not be the same as a name of an attribute renaming or formula but it can be the same as an argument of another formula Furthermore the attribute comparable with types in programming lan guages is an already defined attribute or a renaming of an attribute Such a pair argument name attribute name denotes that the name of the argu ment must be interpreted as a local renaming of the attribute In expressions later on in the formula definition this name can be used as such but only on the right hand side of an comparison see Section 3 5 The list as said before may be empty but the parenthesis are obligatory in all cases also if the list is empty The description of a formula A description of a formula is the part of the formula definition in which you can inform the user of your defined formulae what the meaning
39. more elaborate Now the import has succeeded as you can see in the message pane at the bot tom of the ProM framework window Parsing complete home htdebeer TestLTL testii ltl imported Of course you will see the path and filename of your imported file but the message is clear If the import does not result in success a message is also given in the message pane Importing of home htdebeer TestLTL testO1 1tl aborted In the message pane under the tab error can you find the error message which gives the reason why or a hint how to solve the problem For more information about the parse error messages have a look in the next chapter 2 3 Using the stand alone LTL Parser Happily the LTL Parser is also available as a stand alone program so for debug ging your own LTL Template files you do not need to start ProM The stand alone LTL Parser can be started by typing the following on the command line assuming you are in the base directory of ProM java classpath lib plugins ltlchecker jar org processmining analysis ltlchecker parser LTLParser file to parse When you are using the DOS operating system you have to change the slashes into backslashes The LTL Parser expects exactly one filename If the parsing is successful no message is send to standard out the prompt returns directly If there is an error while parsing a message is send to standard out consisting of the kind of error and on the next line the message of the
40. nces 27 to s instanci ml 187 18 Incorre nces 920 to 14 263 G6 XML log file E 283 283 H 289 289 319 319 324 G24 41 342 342 F 3 AG LAG 1 complete Figure 2 12 Exporting the results logs and visualizations Exporting of the results both the lists with instances and the visualizations is very easy As in Figure 2 12 can be seen just go to the File menu sub menu Export and click on the desired export A save dialog is displayed then in which you can give a name and a place to save the export to 2 9 Reusing the results The ProM framework Convert Window Help orrect instances 27 using Default LTL Checker Plugin Correct process instances 27 Incorrect a eee Figure 2 13 On the results the LTL Checker analysis can be done again with the Default LTL Checker plugin It is possible to use the results of a check again in the ProM framework for example as input to the LTL Checker plugins Both the Default LTL Checker plugin Figure 2 13 and the normal LTL Checker Plugin Figure 2 14 can be applied on a result log either the list with the correct instances or the list with the incorrect instances 14 The ProM framework File Mine Analyse Convert Window Help Perform analysis Petri net Analysis Log Replay Analysis Analysis LTL Checker Plugin Correct instances Heuristics net diff union za gt
41. nghua alpha algorithm plugin Correct instances Q7 using Case data extraction plugin Incorrect instances 920 using V Case data extraction plugin Correct instances 27 using No mining action Incorrect instances 920 using No mining action Correct instances 27 using Social network miner Incorrect instances 920 using Social network miner Log Summary Mining plugin documentatior Figure 2 15 On the results the LTL Checker you can also run a mining algo rithm Not only the LTL Checker plugins can be used on the result logs other plugins can be used too For example the mining algorithms In Figure 2 15 you see the Mine menu containing all the possible combinations of result log and mining algorithm just choose the desired item to start the mining 16 Chapter 3 The Language to specify LTL Properties a reference 3 1 Introduction Using the Default LTL Checker plugin or the LTL Checker plugin with LTL Template files created by others is easy as you have read in the previous chapter Writing your own LTL Template files is another matter This chapter tries to give a full and complete overview of the LTL Language so that you can specify your own LTL properties Before the language itself is explained the environment the language oper ates in is given 3 2 The Environment in which the Language op erates The LTL Language specifies properties of workflow logs of processes A proc
42. oint numbers only Examples are 12 12 34 12 34e5 9E 23 and 123444 You define a number attribute for data element data element as follows number pi data element or number ate data element depending on the scope of the data element 20 e string Attributes of type string are attributes which contain string values Be cause in the log itself all data elements are strings string attributes can be used for all data elements No extra parsing is needed from the data element to an attribute But when you want to use special properties of dates numbers or sets it is a good idea to define data elements of the re spectively type For the string type a special regular expression operator is available Subsection 3 5 2 You define a string attribute for data element data element as follows string pi data element or string ate data element depending on the scope of the data element e set The set type is used for quantification because quantification can only be used on set type attributes For every set attribute a real set containing all the unique values of this data element of all process instances and all audit trail entries is created An extra set operator is the in operator Subsection 3 5 3 You define a set attribute for data element data element as follows set pi data element or set ate data element depending on the scope of the data element e date The last type is the date type It can be used to access
43. plied with a value of type A either an attribute itself the same modulo renaming or a literal of the same type as the attribute 26 You call a formula by entering the name followed by a parameter list sur rounded by parenthesis this list may be empty according to the definition of the formula to call The value of an argument in a call is bound at that place With this feature you get the value of a data element of an attribute of the audit trail entry that is current at the place the argument is used If in the formula a nexttime operator is used the current audit trail entry becomes the next one but the value of the argument supplied to this formula stays the of the current one This early binding can be useful when using the nexttime operator Sub section 3 8 1 because then the current audit trail entry becomes the next one if there is a next one of course With a formula call you can supply such nexttime operator with a value of a attribute before the then current So you can apply recursion of a sort But you will read more on this subject in the subsection about the nexttime operator Examples Because our running example has only one formula defined yet we call it here in a new defined formula version 0 4 Hens This part of the file is as in example version 0 2 VERS Formulae Ht formula eventually task
44. rect too of course In a table A B CA B 010 0 011 1 1 0 1 Yd 1 If the and operator in the last example is replaced with an or operator it stays true in the current audit trail entry It is even true in the third audit trail entry where the person is John too 3 6 4 Implication The proposition A gt B is false if and only if A is true and B is false But be aware the arrow denotes a logical value not a causal relation or a time relation at all When one wants to state something about relations in time thus that if A holds next time should hold B use the nexttime operator _0 In a table AB CAES 010 1 0 1 1 110 0 Ill 1 If a property is only important if another property hold for example a birth date must be before 2000 06 05 when the task is driving That is a person must be old enough to be permitted to drive a car the implication is useful task driving gt bdate 2000 06 05 But if driving does not hold the property with the implication is true If you want to ensure that the 34 task is driving and if the task is driving then the date is lesser than some value use the and operator task driving bdate 2000 06 05 3 6 5 Bi implication The proposition A lt gt B is true if and only if A and B have the same value This operator is also known as equivalence In a table ABA CA xm B 010 1 0 1 0 110 0 111 1 As a example state that a non empt
45. rkflowModelElement set ate riginator date ate dob yyyy MM dd number ate distance string string string number ate question ate answer pi name pi case HH Renamings HH rename rename ate ate ate dob as bdate ate ate ate answer as answer pi name as name pi case as case rename rename rename rename rename rename HH Formulae formula eventually_task_A_is_done_by_person_P A dates have the format WorkflowModelElement as task Originator as person distance as distance question as question lt h2 gt Does eventually P task A h2 lt p gt Is there a audit trail entry in a process instance in which person P does task A p lt p gt lt ul gt lt li gt lt b gt A lt b gt is a task of attribute lt i gt ate WorkflowModelElement lt i gt year month day task P person For this argument fill in the task you want to check for li lt li gt lt b gt P lt b gt is a person of attribute lt i gt ate Originator lt i gt Fill in the person you want to know if he or she perform task A li lt ul gt lt p gt lt gt task A person P 40 formula does John drive Does John drive in a process instance eventually task A is done by person P driving John subformula has If the task is asking then there is a answer not equal to the empty string This formula
46. rrect instances and one with incorrect instances On the results window you see first the name of the checked formula Below this text the window is divided into two tabs one with the correct instances and one with the incorrect instances Both tabs have the same structure In the title of the tab between parentheses the number of instances on that tab is given So you can easily see how much instances of the log are correct or incorrect Figure 2 11 On the tab itself you see two parts the actual table with the instances on the left and a visualization pane on the right In this table the process instances are listed the name of the instances exists of the process instance name and between parentheses the rank of the instance in the log Now you can easily see how the correct and incorrect instances are distributed over the log The visualization pane on the right hand side of the log can be used to visualize one of the instances listed in the table Just select an instance and click the Visualize selected button to create a visualization of the instance Both the lists of correct and incorrect instances can be exported or reused as ordinary logs can be Furthermore a visualization can be exported too 13 2 8 Exporting the Results The ProM framework File Mine Analyse Convert Window Help Plugin 77 EL S LTL Checker Plug Export b visualised correct process instance to 3 DOT Recent files gt Correc a
47. rt Window Help EIE E LTL Checker Plugin Select formula 1 exists state done two times Description Does a state exists which is done two times after e Is there a state which is done and in the next state too Valuate the parameters m iky E Nama m Cancel Figure 2 10 The actual checking is going If you have set the check option you want and the parameters are valuated as you wish you can click the Check button to start the actual check Figure 2 10 You will find this Check button below the list with formulae so in case you select a formula without any parameters you can then click directly the Check button to start checking By the first check the sets for the defined set attributes are created these sets are reused by next checks and the check starts hereafter While checking the progress of the check is displayed together with the name of the current instance On the figure the names are just numbers but it can be every string If you want to stop the checking just click the Cancel button on the progress window After the check is done a new window is displayed the results window 12 2 7 Viewing the Results G The ProM framework File Mine Analyse Convert Window Help Incorrect process instances 920 Visualize selected Figure 2 11 The window with the results a tab with co
48. running ltl and running xml The first file contains the ltl properties specified this chapter and the second file contains a log to test the properties specified in this chapter 3 3 Definitions and Comments An LTL Template file can consist of four different items comments attribute definitions renamings of those defined attributes and formula definitions Those items can be mixed in any order but a definition can only be used if it is already defined Now the different items are described 3 3 1 Comments Comments are the most simple elements of the language A comment starts with a and the rest of the line after the including the is skipped by the parser as comment It is a good practice to use comments in your LTL Template files to document your files in such a manner that you and others can understand and adapt the file later on also after some time It is very easy to create formulae but to 19 understand them can be more difficult if the formulae becomes more complex then comments can be of great help Examples We start our running example by creating some comment lines with some in formation about the file version 0 0 date 01122004 author HT de Beer HH Of course comments at the start of a file only is not that useful It is also possible to use comments in definitions of formula after attribute definitions th
49. scription pane you will see the description if any of the selected formula Figure 2 8 If the imported LTL Template file is created with care there should be a description for every formula If not just guess what the meaning is of the selected formula The third part of the window is the parameter table If the selected formula has any parameters these parameters are shown in this parameter table Figure 2 9 10 The ProM framework File Mine Analyse Convert Window Help E3 Results simple log xml No mining action SS RO ROR RTE ESSENSE NT ESTAN Analysis Default LTL Checker Plugin ZEE Check options Check whole process Check till first failure Check till first success Description Does state B occur after state A occur Compute if there is a state with name A and then the next time there is a state with name B Arguments A of type set ate WorkflowModelElement e Bof type set ate WorkflowModelElement Valuate the parameters Name type a string B type a string Figure 2 9 Fill in some parameters in the Template GUI It is up to you to fill in the values you want for the different parameters Every row of the table exists of three columns a name a type and a value Initially every parameter has an initial value For number attribute parameters it is 0 0 for date it is the date
50. son of the current audit trail entry is either John Mary or Angilbert In this case it results true because in the current audit trail entry D the person is John 3 5 4 The date type literals The type date has no extra operators but the literals themselves are more powerful In principle they are string literals too but are interpreted with the by the date attribute on the left hand side of the operator associated date pattern Those date patterns are explained before Subsection 3 3 2 3 5 5 The number type literals and expressions On the type number there are no extra comparison operators defined but more complex numerical expressions are possible Number literals are either integers or floating point numbers That is just digits or digits with a period and eventually an exponent for example 123 0 4500988 or 314 9067E234 The numerical operators are the well known ones and The unary operator is used as value and the binary ones as value op value The placing of parenthesis are a little bit strange and strict but they are strict too by the logical operators Values can be either numerical expressions number attributes or renamings or arguments or number literals 3 5 6 Examples To the running example some helping formulae are defined with using some comparison operators and literals Because those comparisons are combined to l larger expressions with logical operators
51. subformula moving P person 41 Compute if person P is moving person P N task driving M task cycling V task flying subformula asking P person Compute if person P is asking lt gt person P task asking formula moving_or_asking All persons are either moving or asking around forall p person moving p C asking p 2 2 V C noving p N asking p 1 subformula end nly in the last state holds that in the next state a WorkflowModelElement is not equal itself for other elements the same of course because in the next audit trail entry of the last state all comparisons are false the data elements does obviously not exist ate WorkflowModelElement ate WorkflowModelElement subformula next older d bdate Is d bigger or equal the current date 0 bdate lt d formula always nexttime older Holds always that the birth date of the person in he next audit trail entry is lesser or equal to the date of birth of the person performing the current audit trail entry C C next older bdate end formula move till questionO task asking U distance gt 3 8 6 Parse errors No errors specified 42 Chapter 4 Grammar of the LTL Language 4 1 Literals integer literal 1 9 0 9 x real literal 11 10 9 C
52. ta pattern ordate ate data element date pattern depending on the scope of the data element An attribute can only be defined and used if there is a corresponding data element All data elements you want to query about should be defined as an attribute also the standard data fields like WorkflowModelElement Event Type Timestamp and Originator That these elements are treated separate from the other data elements in the logs does not mean they are treated special in the LTL Checker and LTL Language In fact in the LTL Language all data elements the standard ones too are treated the same Examples Back to our running example of figure 3 2 As you can see in this figure a number of attributes are available in the log In this example we define all the attributes ate WorkflowModelElement ate Originator ate dob ate distance ate question ate answer pi name and pi case version 0 1 date 01122004 author HT de Beer HH HH Defining attributes HH set ate WorkflowModelElement set ate riginator date ate dob yyyy MM dd Date of birth dates have the format year month day number ate distance string ate question string ate answer string pi name number pi case Parse errors e Identifier is already defined Occurs when you tries to define an attribute with the same name as an other earlier defin
53. tents of the string is written down In principle every character can be in the string only quotes themselves are not permitted because they close the literals For example Hello world or 980u908009ud0f098s048uf0u8sd0ff8us09d are both correct strings For strings there is an extra operator the regular expression operator This operator has as string literal a string which is interpreted as a regular expression pattern Internally the matches method of the Java String class is used so if you want to know all the details of the patterns have a look at http java sun com j2se 1 4 2 docs api java util regex Pattern html sum Now follows a short introduction of regular expressions With regular ex pressions you can specify patterns of characters using special regular expression operators Operator Meaning Example A arbritrary character ma like may mad man mau The start of a line The end of a line regexp Zero or one time regexp ma ma regexp One or more times regexp mat ma mama mamama regexp Zero or more times regexp ma ma mama mamama regexpx y Between x and y times regexp mal 2 ma mama rel re2 rel or re2 ma pa pa or ma relre2 rel followed by re2 mapa mapa mamapa mamamapa rel Group rel ma pa ma mama mapama x y Element of x y 1 9 0 9 2 a number like 9 83 3859 abc Element of abc dmy 1 9 43 y5 m5 m3 With the building blocks given in this tabl
54. tself for other elements the same of course because in the next audit trail entry of the last state all comparisons are false the data elements does obviously not exist ate WorkflowModelElement ate WorkflowModelElement Using this end formula it is also possible to specify properties relative to the last state if needed 3 8 2 Eventually The eventually operator checks if a property A does at least once occur in the sequence of audit trail entries of a process instance With lt gt A you write an eventually expression down Remark the correspondence with the exists quantor but this eventually operator is about audit trail entries and the exists quantor about a set 38 In the running example it is clear that lt gt person John holds there are audit trail entries with person is John one of them the current audit trail entry Given this current audit trail entry the expression lt gt task asking is true to because the next audit trail entry is a asking 3 8 3 Always C A Express that A always thus in all audit trail entries of a process instance hold This operator can be compared with the universal quantification as the eventually operator with the existentional T his operator is true on the empty sequence or on the audit trail entry after the last one Use this operator to express that in all audit trail entries a property hold for example that every next audit trail entry the dat
55. xpressions task asking person Mary date 1998 05 22 task 7 cycling task driving person John person John date 2038 12 02 date 2038 12 02 question Where am I distance 8 edistance 103 54 answer Eindhoven name Just a process instance case 234 Figure 3 4 Again the example process instance The explanation of the logical operators is done with the use of the running example where the current audit trail entry is as it was before D Figure 3 4 jk 3 6 1 Not The proposition 1 A is true if and only if A itself is false In a table A CA 0 1 1 0 33 As an example let A be answer Eindhoven Now A is false because there is no answer data element in the current audit trail entry D so answer Eindhoven is true But the reverse holds too let A be distance 1000 with the distance equal to 103 54 you will see easily that the expression distance lt 1000 results in false 3 6 2 And The proposition A B is true if and only if A and B are together true In a table A B CA AB 010 0 011 0 110 0 Ill 1 A simple exampleis task driving person John which is true In the next audit trail entry this would be false both the task and the person are different namely asking and Mary 3 6 3 Or The proposition A B is true if and only if A or B is true if both are true it is cor
56. xttime 38 Parse errors 42 Until 39 LTL Checker Plugin Default How to start 8 Exporting the results 14 How to use the Template GUI 10 LTL Checker Plugin How to start 9 Reusing the results 14 Viewing the results of a check 13 LTL Language 17 Comments 19 Comparisons 28 Date 31 Defining attributes Date 21 Number 20 String 21 Formula definitions 24 Description 24 List of arguments 24 Grammar 43 45 LTL 37 Always 39 Eventually 38 Nexttime 38 Until 39 Name 23 Number 31 Propositional logic 33 And 34 Bi implication 35 Implication 34 Not 33 Or 34 Quantification 35 36 Renamings 23 Running example 19 Set 31 String 30 LTL language Environment 17 LTL Parser Error messages 7 Use on the command line 7 LTL Template Import Plugin How to use 5 Propositional logic 33 And 34 Bi implication 35 Examples 35 Implication 34 Not 33 Or 34 Parse errors 35 Quantification 35 36 Renamings 23 Examples 23 Parse errors 24 Results window 13 Standard LTL Template file 9 Template GUI 10 46
57. y question is equivalent with a empty answer Thus if both are not in the current audit trail entry or both are empty then it is true If one of the data elements answer or question is empty or does not exist then it is false If both does exist and are not empty it is true too question lt gt answer This is true in the current and the next state too 3 6 6 Examples In our running example we have already used some propositional logic operators in the next two sections the logical operators are also used so for now no addition to the running example 3 6 7 Parse errors No errors specified 3 7 Quantificational Logic Quantification in this language exists of the universal fora11 and existentional exists quantor The meaning of quantification is in this context not that clear or to say it otherwise formulae defined in this language can be seen as universal quantification over all process instances of the log Furthermore the LTL operators always 1 and eventually lt gt can be compared with respectively the universal and the existentional quantor because if there exists an audit trail entry with property A then eventually holds A And if always holds A then for all audit trail entries hold A But quantification is not directly about audit trail entries but over sets so the comparison between those LTL operators and quantification is not complete there are properties which can not be specifie
Download Pdf Manuals
Related Search