jtlv-developers Mailing List for JTLV - formal framework
Status: Beta
Brought to you by:
sya
You can subscribe to this list here.
2008 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
(1) |
Jul
|
Aug
|
Sep
(1) |
Oct
(1) |
Nov
|
Dec
|
---|---|---|---|---|---|---|---|---|---|---|---|---|
2009 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
(1) |
Oct
|
Nov
|
Dec
|
2017 |
Jan
|
Feb
|
Mar
(1) |
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
From: Xiangyu L. <lu...@16...> - 2017-03-18 02:32:04
|
Dear all, I am the developer of a BDD-based temporal epistemic model checker MCTK (https://sites.google.com/site/cnxyluo/MCTK/). I found that JTLV is a good platform for developing symbolic verification algorithm and plan to reimplement and extend MCTK based on JTLV. I want to extend the syntax of SMV input language and add some new temporal or modal operators to the existing temporal logics, so I need the AntLR grammar files (SMV.g and SPC.g) of JTLV. Could anyone please send me these grammar files if you like? Thank you in advance and look forward to you reply. Best regards, Xiangyu Luo College of Computer Science & Technology, Huaqiao University, Xiamen, China |
From: Yaniv S. <yan...@gm...> - 2009-09-10 18:16:10
|
Hi to all JTLV users, (and some potential ones...) I'm happy to announce that *JTLV 1.4.0 is out.* (Homepage http://jtlv.sf.net <http://jtlv.sf.net%20>) It has been a while since JTLV's last release, and it is time to publish a new one. The new release contains many new functionalities and bug fixes. Release 1.4.0 includes: * Major parsing refactoring. Fixed many parsing issues. * New declaration for loops, and expression for loops. * An API to replace the under underlying BDD manager. Using JavaBDD interfaces you can now seamlessly plug a new BDD manager to JTLV. * Multi threading support to CUDD package. You can now implement multi threaded symbolic algorithms using the default BDD package or CUDD. (Thanks to Kedar Namjoshi for his help). * Performance improvements. The improvements should apply to all BDD package integrations, specifically to the CUDD package. * Bug fixes for several known issues. * JTLV is now tested and verified on Eclipse Version: 3.5.0, Build id: M20090611-1540. Please refer to the download page to get the latest release. You can find an explanation for the new for loops at FAQ page. Release 1.4.0 has few known limitations: * Declarations for loops are not working in the VAR section! * Since 1.4.0 changed the JNI, we had to compile the BDD libraries all over again. Since we don't have available Mac OS, we could not compile the low level C libraries for that platform. Thus, Mac user will not be able to executed low level C libraries (this issue does not include the pure Java - default - BDD libraries). If anyone has a Mac OS, we will be more then happy to walk him through the compilation steps, and help him get the libraries compiled (and contribute to other Mac users) In our next phase of development, we are going to concentrate our effort on performance issues. If anyone has a test case for which he thinks there might be a performance issue, please send it to us Thanks, and enjoy -- -- yaniv sa'ar :: www.wisdom.weizmann.ac.il/~saar<http://www.wisdom.weizmann.ac.il/%7Esaar> |
From: Yaniv S. <yan...@gm...> - 2009-02-16 23:55:12
|
Hi all, (JTLV users, and potential ones) I am happy to announce JTLV 1.3.2 release (home site<http://jtlv.sourceforge.net/> ). (Please help me spread the word, and forward this mail to anyone you think might be interested...) In addition to many bug fixes 1.3.2 also includes: * New and much more extensive Java Docs. * More usage example in the library. * Procedurally instantiating a module with parameters. * New methodology and interfaces, for users algorithm. * More algorithms implementation in the library. * Better print outs for BDD's and BDDVarSet. * Improved multi threading support. Enjoy, -- -- yaniv sa'ar :: www.wisdom.weizmann.ac.il/~saar<http://www.wisdom.weizmann.ac.il/%7Esaar> |
From: Yaniv S. <yan...@gm...> - 2008-10-31 16:33:58
|
Hey everyone, I have just released JTLV 1.2.1. ( http://jtlv.sourceforge.net ) It contains few bug fix to the error markers in window platform... Since I have seen that many of you are using windows, I have also published a two parts video tutorial, explaining: - part 1 - how to install on windows. (5 minutes video) - part 2 - how to get started. (20 minutes video) This release also contains few feature which I had planed for 1.3.0: - Manual BDD variable ordering. (during pre-load of a SMV file, or at any runtime point afterwards) - New wizards to open new "JTLV Project", "SMV File", and "SPC (Specification) File". - Improved JTLV Project look and feel. Still more to come in 1.3.0 release... Enjoy,... -- -- yaniv sa'ar :: www.wisdom.weizmann.ac.il/~saar |
From: Yaniv S. <yan...@gm...> - 2008-09-28 00:01:34
|
Hi all, (users, and potential ones) I am happy to announce JTLV Formal Framework 1.2.0 release (home site<http://jtlv.sourceforge.net> ). (Please help me spread the word, and forward this mail to anyone you think might be interested...) JTLV now contains many new feature, such as: * New temporal specification parser (Future and Past LTL, CTL, RealTimeCTL, CTL*), with a corresponding advance eclipse editor for specification files, *.spc. The syntax itself is almost identical to NuSMV specification section syntax (JTLV can parse terminal expression a little better in the sense that it can parse any kind of boolean or arithmetic BDD expression, while as in NuSMV you can use arithmetic expressions only in PSL specifications). The editor Includes syntax highlight, on the fly error indicator, on the fly BDD indicator, and much more. (on the fly indicator means, every time you do save, your parsing errors are marked in the editor) * Java API to load and quire the specifications. * The library now also includes various kinds of basic model checking implementations. * Multi threading support. (The ones interested, please contact me first for further instructions) * Standalone release which allows the user to integrate JTLV into his favorite Java editor, or to use JTLV through the prompt. - The release also contain code refactoring, and bug fixes. Including old, previously released features (for the ones not updated) such as: * SMV parser, with a corresponding advance eclipse editor for *.smv files. The syntax itself is almost identical to NuSMV modules syntax, without the specification sections. The editor Includes syntax highlight, on the fly error indicator, auto edit features, and much more. * Java API to load and quire the modules and their entities. * On the fly BDD package arbiter, which allows the user to switch between many BDD packages while running the same algorithm. You can find almost all currently known open source BDD packages - BuDDy, JavaBDD, CUDD, CAL, JDD, ... * Library containing basic implementations such as: shortest path, reachable states, feasible states, GRGames, etc. * An extensive JavaDoc for the library. The JavaDoc engine generated the JTLV user API published here<http://jtlv.sourceforge.net/resources/javaDoc/API1.2.0/index.html>, and gives on the fly method descriptions while programming in your eclipse environment. So how do you get started...? If you have already installed previous releases, then please first uninstall them by: * un-toggling the "JTLV X.X.X Nature" first (Right click or the project) * delete JTLV jar file at <eclipse installation folder>/plugins/JTLV*.jar Next do the installation... * Download eclipse classic distribution 3.3.2 or 3.4.1 (eclipse downloads<http://www.eclipse.org/downloads/> ) * Install eclipse (just unzip the downloaded file...) * Download JTLV 1.2.0 (JTLV downloads<http://sourceforge.net/project/downloading.php?group_id=221922&use_mirror=osdn&filename=jtlv1.2.0.zip&51836585> ) * Install JTLV (just go to the <eclipse installation folder>/ and unzip jtlv1.2.0.zip - a new file "JTLV_1.2.0.jar" will be added to <eclipse installation folder>/plugins/) And that's it.....! Open eclipse, start a new java project, right click the project and toggle the "JTLV 1.2.0 Nature" button and you are ready to go. You can now: * Edit modules in a new *.smv file in your project. * Edit specification in a new *.spc file in your project. * And Implement your formal algorithm in !! Java !! while: - loading the designs you have just created. - loading the specifications you have just created. - choosing what ever BDD package you wish, even ones which are are actually running an efficient C code (by using an underlying JNI to these BDD packages) - using the most advanced state of the art Java programming environment. - sharing and reusing previously implemented formal algorithms through the provided library. (which I hope will grow with time, and your kind help...) - and most importantly, without having to understand the mess, and the native C code... of the formal framework you have otherwise tried to implement your formal algorithm upon. And this is all while still programming in an efficient framework. You are more then welcome to use/join JTLV forums, mailing lists, or other facilities: JTLV Developer forum at - http://sourceforge.net/forum/forum.php?forum_id=800282 JTLV Users forum at - http://sourceforge.net/forum/forum.php?forum_id=800281 Register to JTLV developers mailing list at - https://lists.sourceforge.net/lists/listinfo/jtlv-developers Register to JTLV users mailing list at - https://lists.sourceforge.net/lists/listinfo/jtlv-users JTLV project page at sourceforge at - http://sourceforge.net/projects/jtlv JTLV home site at - http://jtlv.sourceforge.net Or simply mail me for anything.... Enjoy... -- -- yaniv sa'ar :: www.wisdom.weizmann.ac.il/~saar |
From: Yaniv S. <yan...@gm...> - 2008-06-11 18:38:34
|
Hi all, And welcome to our mailing list... (Parth, please register to our developers mailing list) I'll will try to make some sort of a general mail once every two weeks or so, just to keep everyone up to date (kind of like weekly meeting) ============== my personal schedule. Unfortunately, I won't be available by mail this week 12.06 till 18.06, And the two weeks 26.06 till 09.07. I hope you'll manage to start playing with JTLV in your own branches. ============== CVS The CVS is now up again for committing. I still need to install a permissions script to our CVS. PLEASE DO NOT MERGE ( / commit) anything to "HEAD" and "devel_*" branches. You can create your own branches, based on "devel_1_2_0", and commit into your own branches as much as you'd like. (try to name the branches starting with your initials, so we'll know which is whose) ============== new regression I have set up parts of the regression. (If you already created a branch based on "devel_1_2_0", then just do "UPDATE" to your branch, and you'll see our new regression) It currently contains only legacy test cases (inherited from the NuSMV regression) Please add as much testcases as you'd like. (just try to be clean...) You can find there a template for adding a test to the regression. All the regression is under JTLV_IDE/regression component at package "edu.wis.jtlv.regression". To run the regression, right click the java class "AllTests.java" at that package, and go to "Run As"->"JUnit test". (all tests suppose are passing...) ============== new priorities We have two new major candidates to start engaging with JTLV. The first is Doron Peled and few of his students - Doron is well known researcher in the field of formal verification. The other is my supervisor Amir Pnueli who wishes to make a course based on JTLV - this is a great opportunity for massive QA. (and another two of Amir's students) In order for them to start, they MOST HAVE few things Their deadline to see if they can engage with JTLV is the end of Sep. 1. The first and most important component that we need is the specification. I'll start closely working with Hector on that component. Hector, I have setup a basic interface for specification in devel_1_2_0 branch. See what you can do until I'll get back. The good thing is that it is not suppose to be too difficult, since the specification are just a basic composite structure. (They don't have any procedural meaning. Their meaning is given to them by the algorithms...) We have to first construct a solid Java building stones (the composite structure). And then we can go a head with the parser. 2. The second thing to do in our priority is implement model checking algorithms (I think that I'll have to do that personally) 3. The third MOST HAVE, is an SPL to SMV compiler. Parth, I still haven't received any replay from you, are you interested in taking this part? Since I won't be responsive this week, attached is an old implementation for this compiler. Try to read it (specifically, splc.l and splc.y) and see if you can understand what SPL is. ============== Please ask any question.... I'll try to find mail, and if not, I'll answer when I'll get back. Have a nice weekend... Thanks, -- yaniv sa'ar :: ~www.wisdom.weizmann.ac.il/~saar |