[Avispa-users] Suggestions: user-defined functions

[Luca Compagna]

Dear Ben,

I am going to answer to you as developer of SATMC and in name of the
AVISPA team.  The idea behind the prelude file has been quite
controversal during the project. 

Ben Smyth wrote:

>Dear AVISPA users,
>
>I am currently working with AVISPA and would like to make a suggestion for
>future development.
>
>My work requires more than the basic functions that AVISPA provides (such as xor
>and exp), thus supporting user-defined functions would be highly desirable.
>
>According to the documentation it would appear that this is already possible, by
>editing the prelude.if file, however this seems not to be the case. SATMC
>appears to be the only translator which uses the prelude.if file, all other back
>ends simply ignore it? Thus making it impossible to define one's own functions?
>If this is not the case I would be grateful if you could provide me with further
>information.
>  
>
At the beginning we have in mind what you are saying that is to allow
the user to modify the prelude file as he prefers.  Then we figure out
this was not so simple for the majority of the modules (translator and
back-ends) in the AVISPA tool and thus we decide to not allow the user
to change the prelude file i.e. the translator and the back-ends
assume what there is written in the prelude file.  So you may ask why
to introduce a prelude file and I would say for making explicit the
assumption made.  

SATMC (and maybe TA4SP) are the only back-ends that currently process
the prelude file, but I am afraid they both do not support equations.
We would like extend SATMC with algebraic equations and we plan to
work on it in September (a preliminary work in this direction was
started one year ago, but afterthat we did not have resources for
continuing it). 

On the one hand I agree with you that the tool should be extended for
allowing users to specify their own equational theory, goal facts,
etc.  On the other it is not so obvious to implement a back-end able
to consider a generic equational theory.  I am quite sure that on this
specific point my project colleagues at INRIA and ETHZ are more
prepared than me and so I would invite them to express their opinions.

>Further to the above comment I would like to add; the prelude.if file is not the
>best place to put user-defined functions (for numerous reasons, which I won't go
>into here - although feel free to ask). Ideally I would suggest the inclusion of
>the keyword import/include within the hlpsl specification, which defines the
>inclusion of a user-defined prelude (in addition to the default prelude.if).
>Alternatively the additional prelude could be specified at the command line. Or
>both options could be incorporated. Personally I would prefer the include/import
>option.
>  
>
This is a good suggestion and I agree with you that it would be a nice
improvement of the AVISPA tool. 

best regards,
Luca Compagna

P.S. next week the majority of the AVISPA members (me included) will
be quite busy for the project evaluation meeting.  After that I will
be willing to continue this discussion.


>Regards,
>
>Ben Smyth
>
>
>PS - I apologise if you receive this email twice. I have just sent it prior to
>completing the sign up to this list (and it was bounced), hence why I am
>resending.
>
>_______________________________________________
>Avispa-users mailing list
>Avispa-users at avispa-project.org
>http://www.avispa-project.org/mailman/listinfo/avispa-users
>
>  
>

-- 
 Luca Compagna
 PhD student
 E-mail: compa at dist.unige.it    
 E-mail: compa at dai.ed.ac.uk
 http://www.ai.dist.unige.it/compagna
=======================================================
 DIST - University of Genova
 Viale Causa 13, 16145 Genova, ITALY
 phone:  ++39.(0)10.353-6567
 fax:    ++39.(0)10.353-2948
=======================================================
 School of Informatics - University of Edinburgh   
 Appleton Tower, Crichton Street, EH8 9LE Edinburgh, UK
=======================================================