Commit 50a27d8f authored by Michael Weber's avatar Michael Weber
Browse files

LTSmin backend for DiVinE

Squashed commit of the following:

commit 8f10dd78578f6477eb1d682ba113ce947faa9011
Author: Elwin Pater <elwin.pater@gmail.com>
Date:   Fri Aug 13 20:07:24 2010 +0200

    Made transition_info thread-safe

commit 19f112a444aae008d7b80c14f48c848f97157e8d
Author: Elwin Pater <elwin.pater@gmail.com>
Date:   Wed Aug 4 17:07:27 2010 +0200

    Made get_successor(s) compatible to all/long calls

commit 7f122667bcccf12327245dea318f8494a7d4d85a
Author: Elwin Pater <elwin.pater@gmail.com>
Date:   Mon Aug 2 14:50:04 2010 +0200

    Added transition_info to callback

        * Modified callback arguments to match ltsmin
        * Added transition info to return a group

commit a80efe88b7d18d6b5d4190c1c6abf00eb7f06be6
Author: Elwin Pater <elwin.pater@gmail.com>
Date:   Mon Aug 2 14:28:08 2010 +0200

    Fixed problems with channels

        * Fixed bug in generating transition effect
        * Fixed bug in generating channel names
        * Slightly better error messages
        * Fixed printf %d warnings

commit 4c5f0c67f09e77fd0aa130fe31076b67ad410b3b
Author: Elwin Pater <elwin.pater@gmail.com>
Date:   Sat Jul 10 16:30:22 2010 +0200

    Fixed read/write matrix bug on sync trans

commit dcf54fb4d9084228e874bd5f4b663933c74baacd
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Sun Mar 28 17:26:43 2010 +0200

    Fix wrapping bug

commit f21826aaffc8a9ed6709b9c2436ef5b95aabec45
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Sun Mar 7 00:28:18 2010 +0100

    Removed generated unused code

commit 4167966aa22656e0eca8b123be8bae1c1fea76b6
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Sat Mar 6 23:30:02 2010 +0100

    Committed states working

        todo: remove some junk code

commit dcae512697534208ce2199e435fbbbcb61e74964
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Sat Mar 6 17:03:42 2010 +0100

    Fixed bug in analyse_transition

        Use ext_trans->second instead of ext_trans->first
        for synchonized transitions

commit 07ca3167143dd96de54634daee7e67396d76c626
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Sat Mar 6 16:06:48 2010 +0100

    Added ltsmin implementation of get_successor

        TODO: bug: all non-committed transitions can still be active after
              a committed transition.

commit f45d2c62df7dfd2e7dbf5c822e50b51f7f82a380
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Thu Mar 4 22:36:50 2010 +0100

    Output 32 bit struct

        * Note: this introduces a bug, for example a byte
          should wrap and now it doens't

commit bbba53faa4bedfc60d255499ef16742e4d60cfcd
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Thu Mar 4 22:03:01 2010 +0100

    Changed output extension to dve2C

commit 8555a359df7295ac071f0209d10c4995b4fce4ac
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Thu Mar 4 21:53:07 2010 +0100

    Unified library function names

        * added get_ to some function names

commit e2b04f72ff80d144aa7cab22f50ea6aaec05779c
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Thu Mar 4 21:34:13 2010 +0100

    Added state_variable_type function

commit 3b7430158de6c25a9da7d1fa9f7452d3fe5b2daa
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Wed Mar 3 18:22:14 2010 +0100

    Added export of type names and values

commit b1c28927a735ce2be1cced016a9744575d6c290b
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Wed Mar 3 16:01:18 2010 +0100

    Added export of state variable names

commit 933cc56a70767016b8c1fa6a32e5a16e57a40ada
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Wed Mar 3 15:11:54 2010 +0100

    Added has_property function

commit a63c85da8361ada0cd4729ceab41f976bd481fa8
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Tue Mar 2 18:19:48 2010 +0100

    Added transition read/write dependency output

commit ea54a419848ad95200a23ee5075b38df33a7ad4b
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Tue Mar 2 11:59:21 2010 +0100

    Added modifications for channels (read/write)

        * Untested

commit 61cc77ae85969e9385b6190ddaaaf0c4fa0bd4d7
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Tue Mar 2 11:30:44 2010 +0100

    Analyse expressions, mark in state vector

        * Fixed channel initialization
        * Added transition effect read/write mark
        * Added transition guard read/write mark
        * Todo: mark channels read/write

commit 84b9e6365552906c4f94f1b1d01cc8d1da39359e
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Mon Mar 1 16:21:02 2010 +0100

    Added dependency output comments

commit 30f567c0c2a661fe52c23f974455ab7748d1fceb
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Mon Mar 1 15:53:45 2010 +0100

    Added state variables count

commit bc3d99a2c953a394f4069dd726e5a5ec73ecef7c
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Mon Mar 1 15:43:45 2010 +0100

    Added mark_dependency function

commit dfe2e310e16eadefdb778b74851d12521c4cdadc
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Mon Mar 1 15:00:32 2010 +0100

    Working get_initial_state for ltsmin

commit 9ed5bc94d393831afbdb5e2432359b034c21d636
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Sat Feb 27 22:09:49 2010 +0100

    Added get_successors with callback function

commit 0692ff5d096a409e15aa93786585cefe7a8928e6
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Fri Feb 26 21:30:25 2010 +0100

    Added --ltsmin option instead of --analysis

commit 2ff390a52a4da0b3a651d9a04eca4cb8d4b4cd3b
Author: Elwin Pater <e.pater@student.utwente.nl>
Date:   Fri Feb 26 18:03:54 2010 +0100

    Added --analysis option
parent 9d33f388
......@@ -25,7 +25,7 @@ set( JARS "${CMAKE_SOURCE_DIR}/nips-compiler-jars/pml2s.jar"
set( PML_C "${CMAKE_CURRENT_BINARY_DIR}/divine.compile-pml" )
set( NIPS_ASM "${CMAKE_CURRENT_SOURCE_DIR}/compile-pml.pl" )
add_executable( divine divine.cpp dvecompile.cpp compile.cpp combine.h ${COMBINE_M4_H} )
add_executable( divine divine.cpp dvecompile.cpp combine.h ${COMBINE_M4_H} )
add_executable( divine.simulate simulator.cpp )
add_executable( divine.simple simple.cpp )
......
......@@ -3,7 +3,6 @@
#include <wibble/commandline/parser.h>
#include <wibble/string.h>
#include "dvecompile.h"
#include <wibble/sys/fs.h>
namespace divine {
......@@ -16,9 +15,17 @@ extern const char *compile_defines_str;
using namespace wibble;
struct Compile {
commandline::BoolOption *o_ltsmin;
commandline::Engine *cmd_compile;
commandline::StandardParserWithMandatoryCommand &opts;
void die_help( std::string bla )
{
opts.outputHelp( std::cerr );
die( bla );
}
void die( std::string bla ) __attribute__((noreturn))
{
std::cerr << bla << std::endl;
......@@ -48,8 +55,8 @@ struct Compile {
run( cmd.str() );
}
void compileDve( std::string in ) {
dve_compiler compiler;
void compileDve( std::string in, bool ltsmin ) {
dve_compiler compiler(ltsmin);
compiler.read( in.c_str() );
compiler.analyse();
......@@ -58,20 +65,29 @@ struct Compile {
compiler.setOutput( out );
compiler.print_generator();
gplusplus( outfile, str::basename( in ) + ".so" );
if (ltsmin) {
gplusplus( outfile, str::basename( in ) + "2C" );
} else {
gplusplus( outfile, str::basename( in ) + ".so" );
}
}
void compileMurphi( std::string in );
void main() {
if ( !opts.hasNext() )
die_help( "FATAL: No input file specified." );
std::string input = opts.next();
if ( access( input.c_str(), R_OK ) )
die( "FATAL: cannot open input file " + input + " for reading" );
if ( str::endsWith( input, ".dve" ) )
compileDve( input );
else if ( str::endsWith( input, ".m" ) )
if ( str::endsWith( input, ".dve" ) ) {
compileDve( input, o_ltsmin->boolValue() );
#ifdef HAVE_MURPHI
} else if ( str::endsWith( input, ".m" ) ) {
compileMurphi( input );
else {
#endif
} else {
std::cerr << "Do not know how to compile this file type." << std::endl;
}
}
......@@ -82,6 +98,10 @@ struct Compile {
cmd_compile = _opts.addEngine( "compile",
"<input>",
"model compiler");
o_ltsmin = cmd_compile->add< commandline::BoolOption >(
"ltsmin", 'l', "ltsmin", "",
"ltsmin interface" );
}
};
......
This diff is collapsed.
......@@ -18,10 +18,13 @@ struct ext_transition_t
dve_transition_t *first;
dve_transition_t *second; //only when first transition is synchronized;
dve_transition_t *property; // transition of property automaton
std::vector<int> sv_read;
std::vector<int> sv_write;
};
struct dve_compiler: public dve_explicit_system_t
{
bool ltsmin;
bool many;
int current_label;
......@@ -60,11 +63,16 @@ struct dve_compiler: public dve_explicit_system_t
outline();
}
dve_compiler(error_vector_t & evect=gerr)
: explicit_system_t(evect), dve_explicit_system_t(evect), current_label(1), m_indent( 0 )
dve_compiler(bool ltsmin, error_vector_t & evect=gerr)
: explicit_system_t(evect), dve_explicit_system_t(evect), current_label(0), m_indent( 0 ), ltsmin(ltsmin)
{}
virtual ~dve_compiler() {}
int count_state_variables();
void analyse_expression( dve_expression_t & expr, ext_transition_t &ext_transition, std::vector<int> &dep );
void output_dependency_comment( ext_transition_t &ext_transition );
void mark_dependency ( size_int_t gid, int type, int idx, std::vector<int> &dep);
void analyse_transition_dependencies( ext_transition_t &ext_transition );
void analyse_transition( dve_transition_t * transition,
vector<ext_transition_t> &ext_transition_vector );
void analyse();
......@@ -127,15 +135,15 @@ struct dve_compiler: public dve_explicit_system_t
}
std::string process_state( int i, std::string state ) {
return state + "." + process_name( i ) + ".state";
return state + "." + process_name( i ) + ".state" + (ltsmin?".var":"");
}
std::string channel_items( int i, std::string state ) {
return state + "." + channel_name( i ) + ".number_of_items";
return state + "." + channel_name( i ) + ".number_of_items" + (ltsmin?".var":"");
}
std::string channel_item_at( int i, std::string pos, int x, std::string state ) {
return state + "." + channel_name( i ) + ".content[" + pos + "].x" + wibble::str::fmt( x );
return state + "." + channel_name( i ) + ".content[" + pos + "].x" + wibble::str::fmt( x ) + (ltsmin?".var":"");
}
int channel_capacity( int i ) {
......@@ -177,10 +185,13 @@ struct dve_compiler: public dve_explicit_system_t
void new_output_state();
void gen_successors();
void gen_ltsmin_successors();
void gen_is_accepting();
void gen_header();
void gen_state_struct();
void gen_initial_state();
void gen_state_info();
void gen_transition_info();
void print_generator();
};
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment