Skip to:

  1. Skip to Jira Navigation
  2. Skip to Side Navigation
  3. Skip to Main Content

List Theory should be supported in ProB 2.0

Description

HOW TO REPRODUCE:
s = api.eventb_load(path/to/machine)
t = s as Trace
t = t.$initialise_machine()
t = t.$add("p = 5")
assert t.evalCurrent("l").value == "5"
t = t.$add("p = 9")
assert t.evalCurrent("l").value == "9"

Standard theories can be found here:
http://wiki.event-b.org/index.php/Theory_Plug-in

This is related to

When attempting to animate a machine using the Theory Plug-in Lists, the following Type error from Prolog is produced (the load command can be found in the attachments):

DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! An error occurred !
2015-09-14 14:37:53,461 5763 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! source(btype)
2015-09-14 14:37:53,461 5763 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! btype failed:
2015-09-14 14:37:53,461 5763 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! recop_create_in_case:extended_expr(none,cons,[identifier(none,x),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))],[])
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! An error occurred !
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! source(btype)
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! btype failed:
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! btype_l:extended_expr(none,append,[identifier(none,l),identifier(none,p)],[])
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! An error occurred !
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! source(btype)
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! btype failed:
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! btype_l:assign(rodinpos('Mch',a,[]),[identifier(none,l)],[extended_expr(none,append,[identifier(none,l),identifier(none,p)],[])])
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! An error occurred !
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! source(internal_error(bmachine_eventb))
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! Internal Error; call failed:
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! typecheck_l([assign(rodinpos('Mch',a,[]),[identifier(none,l)],[extended_expr(none,append,[identifier(none,l),identifier(none,p)],[])])],env(node(operator(head),entry(boolean,[bmachine_eventb:destructor_operator('List'(2755479),[prj1],cons,couple(_2755479,freetype('List'(any))))]),-1,node(operator(conc),entry(boolean,[bmachine_eventb:recursive_operator([argument(l1,extended_expr(none,'List',[identifier(none,'T')],[])),argument(l2,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l1,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),identifier(none,l2)),case(l1,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x),extended_expr(none,conc,[identifier(none,l0),identifier(none,l2)],[])],[]))],['S','T'])]),-1,node(operator('List'),entry(boolean,[bmachine_eventb:freetype_operator('List'(_2755479),[_2755479],[identifier(none,'T')],[used_param_types(cons,[1],[identifier(none,'T'),identifier(none,'List')])])]),-1,node(p,entry(integer,[nodeid(rodinpos('Mch',p,[])),loc('Mch',event(add))]),0,node(l,entry(freetype('List'(integer)),[nodeid(none),loc('Mch',variables),section('Mch'),level(0)]),0,empty,empty),node(operator('COND'),entry(boolean,[bmachine_eventb:direct_definition([argument('THEN',identifier(none,'IFTHENELSETYPE')),argument('ELSE',identifier(none,'IFTHENELSETYPE')),argument('IF',set_extension(none,[truth(none)]))],if_then_else(none,identifier(none,'IF'),identifier(none,'THEN'),identifier(none,'ELSE')),['_IFTHENELSETYPE'])]),0,empty,empty)),node(operator(append),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[])),argument(x,identifier(none,'T'))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),extended_expr(none,cons,[identifier(none,x),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))],[])),case(l,[l0,x0],extended_expr(none,cons,[identifier(none,x0),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x0),extended_expr(none,append,[identifier(none,l0),identifier(none,x)],[])],[]))],['S','T'])]),0,empty,empty)),node(operator(cons),entry(boolean,[bmachine_eventb:constructor_operator('List'(_2755479),[_2755479,freetype('List'(any))])]),1,empty,node(operator(flatten),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,ll0],extended_expr(none,cons,[identifier(none,l0),identifier(none,ll0)],[]),extended_expr(none,conc,[identifier(none,l0),extended_expr(none,flatten,[identifier(none,ll0)],[])],[]))],['S','T'])]),0,empty,empty))),node(operator(nil),entry(boolean,[bmachine_eventb:constructor_operator('List'(_2755479),[])]),0,node(operator(listSize),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),integer(none,0)),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),add(none,integer(none,1),extended_expr(none,listSize,[identifier(none,l0)],[])))],['S','T'])]),1,empty,node(operator(map),entry(boolean,[bmachine_eventb:recursive_operator([argument(f,pow_subset(none,cartesian_product(none,identifier(none,'T'),identifier(none,'S')))),argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'S')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[function(none,identifier(none,f),[identifier(none,x)]),extended_expr(none,map,[identifier(none,f),identifier(none,l0)],[])],[]))],['S','T'])]),0,empty,empty)),node(operator(tail),entry(boolean,[bmachine_eventb:destructor_operator('List'(_2755479),[prj2],cons,couple(_2755479,freetype('List'(any))))]),-1,node(operator(rev),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,append,[extended_expr(none,rev,[identifier(none,l0)],[]),identifier(none,x)],[]))],['S','T'])]),0,empty,empty),empty)))),subst,_4615451,actions)
2015-09-14 14:37:53,462 5764 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! An error occurred !
2015-09-14 14:37:53,463 5765 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! source(internal_error(bmachine_eventb))
2015-09-14 14:37:53,463 5765 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! Internal Error; call failed:
2015-09-14 14:37:53,463 5765 [Thread-4] DEBUG de.prob.cli.ProBInstance Method:
readAndLog Line: 54 - ! check_event(event(rodinpos('Mch',add,[]),add,ordinary(none),[],[identifier(rodinpos('Mch',p,[]),p)],[member(rodinpos('Mch',grd,[]),identifier(none,p),interval(none,integer(none,1),integer(none,10)))],[],[assign(rodinpos('Mch',a,[]),[identifier(none,l)],[extended_expr(none,append,[identifier(none,l),identifier(none,p)],[])])],[]),'Mch',env(node(operator(head),entry(boolean,[bmachine_eventb:destructor_operator('List'(2755479),[prj1],cons,couple(_2755479,freetype('List'(any))))]),-1,node(operator(conc),entry(boolean,[bmachine_eventb:recursive_operator([argument(l1,extended_expr(none,'List',[identifier(none,'T')],[])),argument(l2,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l1,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),identifier(none,l2)),case(l1,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x),extended_expr(none,conc,[identifier(none,l0),identifier(none,l2)],[])],[]))],['S','T'])]),-1,node(operator('List'),entry(boolean,[bmachine_eventb:freetype_operator('List'(_2755479),[_2755479],[identifier(none,'T')],[used_param_types(cons,[1],[identifier(none,'T'),identifier(none,'List')])])]),-1,node(operator('COND'),entry(boolean,[bmachine_eventb:direct_definition([argument('THEN',identifier(none,'IFTHENELSETYPE')),argument('ELSE',identifier(none,'IFTHENELSETYPE')),argument('IF',set_extension(none,[truth(none)]))],if_then_else(none,identifier(none,'IF'),identifier(none,'THEN'),identifier(none,'ELSE')),['IFTHENELSETYPE'])]),-1,node(l,entry(freetype('List'(integer)),[nodeid(none),loc('Mch',variables),section('Mch'),level(0)]),0,empty,empty),empty),node(operator(append),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[])),argument(x,identifier(none,'T'))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),extended_expr(none,cons,[identifier(none,x),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))],[])),case(l,[l0,x0],extended_expr(none,cons,[identifier(none,x0),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x0),extended_expr(none,append,[identifier(none,l0),identifier(none,x)],[])],[]))],['S','T'])]),0,empty,empty)),node(operator(cons),entry(boolean,[bmachine_eventb:constructor_operator('List'(_2755479),[_2755479,freetype('List'(any))])]),1,empty,node(operator(flatten),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,ll0],extended_expr(none,cons,[identifier(none,l0),identifier(none,ll0)],[]),extended_expr(none,conc,[identifier(none,l0),extended_expr(none,flatten,[identifier(none,ll0)],[])],[]))],['S','T'])]),0,empty,empty))),node(operator(nil),entry(boolean,[bmachine_eventb:constructor_operator('List'(_2755479),[])]),0,node(operator(listSize),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),integer(none,0)),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),add(none,integer(none,1),extended_expr(none,listSize,[identifier(none,l0)],[])))],['S','T'])]),1,empty,node(operator(map),entry(boolean,[bmachine_eventb:recursive_operator([argument(f,pow_subset(none,cartesian_product(none,identifier(none,'T'),identifier(none,'S')))),argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'S')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[function(none,identifier(none,f),[identifier(none,x)]),extended_expr(none,map,[identifier(none,f),identifier(none,l0)],[])],[]))],['S','T'])]),0,empty,empty)),node(operator(tail),entry(boolean,[bmachine_eventb:destructor_operator('List'(_2755479),[prj2],cons,couple(_2755479,freetype('List'(any))))]),-1,node(operator(rev),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,append,[extended_expr(none,rev,[identifier(none,l0)],[]),identifier(none,x)],[]))],['S','T'])]),0,empty,empty),empty)))),env(node(operator(head),entry(boolean,[bmachine_eventb:destructor_operator('List'(_2755479),[prj1],cons,couple(_2755479,freetype('List'(any))))]),-1,node(operator(conc),entry(boolean,[bmachine_eventb:recursive_operator([argument(l1,extended_expr(none,'List',[identifier(none,'T')],[])),argument(l2,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l1,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),identifier(none,l2)),case(l1,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x),extended_expr(none,conc,[identifier(none,l0),identifier(none,l2)],[])],[]))],['S','T'])]),-1,node(operator('List'),entry(boolean,[bmachine_eventb:freetype_operator('List'(_2755479),[_2755479],[identifier(none,'T')],[used_param_types(cons,[1],[identifier(none,'T'),identifier(none,'List')])])]),-1,node('l\'',entry(freetype('List'(integer)),[nodeid(none),loc('Mch',variables),section('Mch'),level(0)]),0,node(l,entry(freetype('List'(integer)),[nodeid(none),loc('Mch',variables),section('Mch'),level(0)]),0,empty,empty),node(operator('COND'),entry(boolean,[bmachine_eventb:direct_definition([argument('THEN',identifier(none,'IFTHENELSETYPE')),argument('ELSE',identifier(none,'IFTHENELSETYPE')),argument('IF',set_extension(none,[truth(none)]))],if_then_else(none,identifier(none,'IF'),identifier(none,'THEN'),identifier(none,'ELSE')),['_IFTHENELSETYPE'])]),0,empty,empty)),node(operator(append),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[])),argument(x,identifier(none,'T'))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),extended_expr(none,cons,[identifier(none,x),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))],[])),case(l,[l0,x0],extended_expr(none,cons,[identifier(none,x0),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x0),extended_expr(none,append,[identifier(none,l0),identifier(none,x)],[])],[]))],['S','T'])]),0,empty,empty)),node(operator(cons),entry(boolean,[bmachine_eventb:constructor_operator('List'(_2755479),[_2755479,freetype('List'(any))])]),1,empty,node(operator(flatten),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,ll0],extended_expr(none,cons,[identifier(none,l0),identifier(none,ll0)],[]),extended_expr(none,conc,[identifier(none,l0),extended_expr(none,flatten,[identifier(none,ll0)],[])],[]))],['S','T'])]),0,empty,empty))),node(operator(nil),entry(boolean,[bmachine_eventb:constructor_operator('List'(_2755479),[])]),0,node(operator(listSize),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),integer(none,0)),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),add(none,integer(none,1),extended_expr(none,listSize,[identifier(none,l0)],[])))],['S','T'])]),1,empty,node(operator(map),entry(boolean,[bmachine_eventb:recursive_operator([argument(f,pow_subset(none,cartesian_product(none,identifier(none,'T'),identifier(none,'S')))),argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'S')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[function(none,identifier(none,f),[identifier(none,x)]),extended_expr(none,map,[identifier(none,f),identifier(none,l0)],[])],[]))],['S','T'])]),0,empty,empty)),node(operator(tail),entry(boolean,[bmachine_eventb:destructor_operator('List'(_2755479),[prj2],cons,couple(_2755479,freetype('List'(any))))]),1,node(operator(rev),entry(boolean,[bmachine_eventb:recursive_operator([argument(l,extended_expr(none,'List',[identifier(none,'T')],[]))],[case(l,['T'],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,append,[extended_expr(none,rev,[identifier(none,l0)],[]),identifier(none,x)],[]))],['S','T'])]),0,empty,empty),empty)))),[],[b(identifier(l),freetype('List'(integer)),[nodeid(none),loc('Mch',variables),section('Mch'),level(0)])],[],[b(identifier(l),freetype('List'(integer)),[nodeid(none),loc('Mch',variables),section('Mch'),level(0)])],,_4607253)
2015-09-14 14:37:53,469 5771 [main] INFO de.prob.cli.ProBConnection Method:
send Line: 79 - yes('.'(=('_Error',[]),[]))
2015-09-14 14:37:53,470 5772 [main] INFO de.prob.cli.ProBConnection Method:
send Line: 66 - get_error_messages(WarningsOnly,Errors),true.

Environment

None

Attachments

4

Gliffy Diagrams

Activity

Show:

Jenkins Build Server September 17, 2015 at 2:34 PM

SUCCESS: Integrated in probcore_windows_tests #546 (See http://cobra.cs.uni-duesseldorf.de/jenkins/job/probcore_windows_tests/546/)
trying to get the DataTypes to parse correctly. (clark.joy: rev 6f3251921c26cbf60333e5a0b88ec36dd2ca9bef)

Jenkins Build Server September 17, 2015 at 2:31 PM

SUCCESS: Integrated in probcore_win64_tests #575 (See http://cobra.cs.uni-duesseldorf.de/jenkins/job/probcore_win64_tests/575/)
trying to get the DataTypes to parse correctly. (clark.joy: rev 6f3251921c26cbf60333e5a0b88ec36dd2ca9bef)

Joy Clark September 15, 2015 at 6:47 AM

This is an example of a theory file that can be loaded and animated by ProB. This can be used as a reference in order to generate a correct Prolog translation of the theory plug-in from ProB 2.0.

Details

Assignee

Reporter

Story Points

Fix versions

Priority

Created September 14, 2015 at 11:51 AM
Updated June 30, 2019 at 1:48 AM
Configure