A program code is writen in file program.py This file contains one python function which returns a python tuple (program,env) 'program' is a list of tuples - one tuple = one program line. Each command has own semantic. There are several types of commands. x:=null ("x=null","line_num",x,next_line) x:=y ("x=y","line_num",x,y,next_line) x:=y.next ("x=y.next","line_num",x,y,next,next_line) x.next=y ("x.next=y","line_num",x,y,next,next_line,descr_num) if x==NULL ("ifx==null",line_num",x,next_line_then,next_line_else) if x==y ("ifx==y","line_num",x,y,next_line_then,next_line_else) if * ("if*","line_num",next_line_then,next_line_else) goto ("goto","line_num",next_line) exit ("exit","line_num") x.next=null ("x.next=null","line_num",x,next,next_line) xnext=new ("x.next=new","line_num",x,next,next_line, descr_num, gen_descr) setdata ("setdata","line_num",x,"data",next_line) if x.data=="..." ("ifdata","line_num",x,"data",next_line_then,next_line_else) x:=random_position ("x=random","line_num",x,next_line) new ("new","line_num",x,next_line) ------------------------------------------------ - The first string is a command identificator - line_num: a string of [01]*, it is used inside transducers and state sets. - it is necessary to have different strings for different lines !!! All strings MUST have equal length !!! - Transducer for a given line handle ONLY configurations with corresponding line number. - this string are alse used for bad configuration checking - x, y: pointer variables. It is a natural number (1,2,3,4,...) - next: next pointer identificator. They are numbered from 0 (0,1,2,3,4,...) - next_line: after 'execution' of this line, skip to line number ... Line number corresponds to the position in list 'program'. Lines are numbered from 0 (0,1,2,3,4,5,...) - next_line_then, next_line_else: equal semantics to next_line - descr_num: pointer descriptor used in execution of this command. Descriptors are numbered from 1 (1,2,3,4,...) - gen_descr: automatic generation of initial descriptor used in x.next=null (0 - off, 1 - on) use "1" if you are not sure what you are doing. ################################################################### The basic strategy for use of descriptor numbers is the following: (follow it if you exactly don't know what you are doing) - there are several descriptors used in initial set of configurations - don't use them in program.py - each x.next=y and x.next=new statement gets its own fresh descriptor Descriptors + automatic generation og initial configurations (according to the typedefs) - create file typedefs - run the script "get_typedef_descr.t.sh" to obtain the number of descriptors used in initial configurations - assign unique number to each x.next=y, x.next=new statement Example: There are 3 statements in program.py: x.next=y x.next=new x.next=y The script "get_typedef_descr.t.sh" provides number "4". Then assigh the descriptors as follows: x.next=y - descr_num=5 x.next=new - descr_num=6 x.next=y - descr_num=7 Then set desc_num=8 in "enviroment" (see the following). ################################################################### The variable 'env' is a tuple of the type: env=(node_width,pointer_num,desc_num,next_num,err_line,restrict_var) - pointer_num: number of pointer variables !!! increased by 1 !!! There is a special pointer variable '0', which can pointed to more nodes, it identifies disposed nodes - this is the reason for increment of 1 - descr_num: number of pointer descriptors !!! increased by 1 !!! There is a special descriptor called 'token' with inner use - this is the reason for increment of 1 - next_num: number of next pointers used in program - err_line: error line number - it is usually "111111". Look at 'line_num' in program definition. - restrict_var: Possible values: 0 - off, 1 - on. Automatic generation of automata, which guarrantee only one occur of a program variable in configuration. (Abstraction can cause more than 1 occur in configuration) Use "1" if you don't know what you are doing. - node_width: Maximal node_width. node_width=pointer_num+descr_num+2+data_size ------------------------------------------------------- If you like to use automatic generation of initial configurations, you need to place the following two lines in the top of the program.py file. This lines provides a mapping between symbolic (human readable) names of pointer variables and next selectors and the numbers used in program.py # pointer variables are : x=3, top=1, aux=2 # next pointers are : next=0 back=1 here, the pojnter variable top is described by the number "1", aux by the number "2" and x by the number "3" There are two next pointers: next is described by the number "0" and back by the number "1" *************************************************************************************** Example: Single linked list creation: *************************************************************************************** void create_single_linked_list(void *x) { /* pointer x pointed on the last element of a list - on the beginning we have at least 1 element in a list */ void *y; while * { y=new; x.next=y x=x.next } return; } -------------------------------------------- # pointer variables are : x=1 # next pointers are : next=0 def get_program(): #variable program contains list of commands program=[ ("if*","0001",4,1), # nondeterministic choice of next line ("x.next=new","0010",1,0,2,1,1), # x.0=new, continue on line 2, use descriptor 1, generate corresponding descriptor ("x=y.next","0011",1,1,0,3), # x=x.0, continue with line 3 ("goto","0100",0), # continue with line 0 ("exit","0101") ] # exit() node_width=7 # we have one pointer variable x -> set pointer_num to 2 pointer_num=2 # we have one descriptor -> set descr_num to 2 desc_num=2 # we have only one next pointer. next_num=1 err_line="1111" # we need not restrict automata for this simple program ;-) restrict_var=0 env=(node_width,pointer_num,desc_num,next_num,err_line,restrict_var) return (program,env) --------------------------------------------