// -*- C++ -*- (c) 2013-2015 Vladimír Štill <xstill@fi.muni.cz>

/* ====================== The DIVINE compact file format ======================
 *
 * DIVINE explicit is compact explicit representation of state-space.
 * It can be generated by algorithm gen-explicit, even in distributed way, all
 * parameters that can be passed to divine metrics can be also passed to
 * gen-explicit, for example option to compress state-space when exploring it
 *    $ divine gen-explicit <model> [ --compression=tree ... ]
 * If state space is generated in distributed environment it is
 * expected that output file will be on shared filesystem.
 *
 * Each state in explicit representation is assigned natural number, those
 * numbers are continuous. State with number 0 is virtual state vertex
 * with edges to all initial states of model.
 * This virtual initial vertex is present even in reversed edge encoding,
 * with edges still pointing _toward_ initial states
 *
 * Explicit file format contains
 * - header with meta-information about state-space
 * - encoding of edges in state-space (forward and/or backward)
 * It can also optionally contain
 * - encoding of all reversed edges in state-space
 * - memory of all states
 *
 * Both edges and nodes are encoded in terms of DataBlock object which
 * represents array of variable sized objects. It consists of two arrays
 * (allocated in fact continuously) the first with as many fields of
 * type int64_t as there is nodes in state space. n-th of this fields
 * contains offset of ending of n-th element of array.
 *
 * Edges are encoded by array of destination vertices (index of this
 * array is source vertex), together with label. Their representation is
 * isomorphic to std::tuple< int64_t, Label > where Label can be either
 * uint64_t or empty struct (that is if Label is empty edge encoding is
 * isomorphic to int64_t).
 *
 * Explicit V1 header is 128B long, with fixed format, see struct Header.
 *
 * At runtime, explicit file (with .dess extension -- DiVinE Explicit
 * State Space) is mapped to memory to allow easy access of it.
 * To do this object of type Explicit is used. This object can be copied,
 * but it is shallow copy. File is automatically unmapped when object
 * (all copies) come out of scope. Explicit file is opened either by
 * giving path in constructor or by calling open( string path ) method
 * on object.
 *
 * Writing to Explicit data will result in SIGSEGV or similar if flags
 * for opening are not specified, even then it is thread-unsafe to write here.
 *
 * Because dess files are mapped into memory they are endianity-dependent!
 */

#if GEN_EXPLICIT || ALG_EXPLICIT

#include <type_traits>
#include <brick-mmap.h>
#include <brick-data.h>
#include <vector>
#include <divine/explicit/header.h>

#ifndef DIVINE_COMPACT_COMPACT_H
#define DIVINE_COMPACT_COMPACT_H

namespace divine {
namespace dess {

static_assert( sizeof( Header ) == 152, "Wrong size of Header" );

struct DataBlock {
    DataBlock() : _count( 0 ), _indices( nullptr ), _data( nullptr ) { }
    DataBlock( int64_t count, int64_t *indices, char *data ) :
        _count( count ), _indices( indices ), _data( data )
    { }
    template< typename T >
    DataBlock( int64_t count, T *mem ) : _count( count ),
        _indices( reinterpret_cast< int64_t * >( mem ) ),
        _data( reinterpret_cast< char * >( reinterpret_cast< int64_t * >( mem ) + count ) )
    { }

    int64_t count() { return _count; }

    char *operator[]( int64_t ix ) {
        ASSERT_LEQ( ix, _count );
        return _ix( ix );
    }

    const char *operator[]( int64_t ix ) const {
        ASSERT_LEQ( ix, _count );
        return _ix( ix );
    }

    int64_t size( int64_t ix ) const {
        int64_t diff = int64_t( _ix( ix + 1 ) ) - int64_t( _ix( ix ) );
        ASSERT_LEQ( 0, diff );
        return diff;
    }

    template< typename T >
    T &get( int64_t ix ) {
        ASSERT_LEQ( ix, _count - 1 );
        return *reinterpret_cast< T * >( _ix( ix ) );
    }

    template< typename T >
    struct _MapHelper {
        _MapHelper( char *ptr, int64_t size ) :
            _ptr( reinterpret_cast< T * >( ptr ) ),
            _size( size / sizeof( T ) )
        {
            ASSERT_EQ( 0UL, size % sizeof( T ) );
        }

        template< typename Fn >
        auto operator()( Fn fn )
            -> typename std::enable_if< !std::is_void<
                typename std::result_of< Fn( T *, int64_t ) >::type >::value,
                typename std::result_of< Fn( T *, int64_t ) >::type >::type
        {
            return fn( _ptr, _size );
        }

        template< typename Fn >
        auto operator()( Fn fn )
            -> typename std::enable_if< std::is_void<
                typename std::result_of< Fn( T *, int64_t ) >::type >::value,
                void >::type
        {
            fn( _ptr, _size );
        }

      private:
        T* _ptr;
        int64_t _size;
    };


    template< typename T = char >
    _MapHelper< T > map( int64_t ix ) {
        ASSERT_LEQ( ix, _count - 1 );
        return _MapHelper< T >( _ix( ix ), size( ix ) );
    }
/*
    template< typename T >
    struct Inserter {
        Inserter( DataBlock &db, int64_t from ) :
            _ptr( db._indices + from ),
            _dataNext( reinterpret_cast< T* >( db._data + (from == 0 ? 0 : _ptr[ -1 ]) ) ),
            _dataBlock( &db )
        { }

        template< typename... Args >
        T& emplace( Args &&... args ) {
            new ( _dataNext ) T( std::forward< Args >( args )... );
            T &r = *_dataNext;
            ++_dataNext;
            *_ptr = reinterpret_cast< size_t >( _dataNext )
                - reinterpret_cast< size_t >( _dataBlock->_data );
            ASSERT_LEQ( 0, *_ptr );
            ++_ptr;
            return r;
        }

      protected:
        int64_t *_ptr;
        T *_dataNext;
        DataBlock *_dataBlock;
    };

    template< typename T >
    Inserter< T > inserter( int64_t from = 0 ) {
        return Inserter< T >( *this, from );
    }
*/
    struct FInserter {
        FInserter( DataBlock &db, int64_t from ) :
            _ptr( db._indices + from ),
            _dataNext( db._data + (from == 0 ? 0 : _ptr[ -1 ]) ),
            _dataBlock( &db )
        { }

        FInserter() : _ptr( nullptr ), _dataNext( nullptr ),
            _dataBlock( nullptr )
        { }

        template< typename Fn >
        auto emplace( int64_t size, Fn fn )
            -> typename std::result_of< Fn( char *, int64_t ) >::type
        {
            ASSERT( _ptr ); ASSERT( _dataNext ); ASSERT( _dataBlock );
            char *data = _dataNext;
            _dataNext += size;
            *_ptr = _dataNext - _dataBlock->_data;
            ++_ptr;
            return fn( data, size );
        }

      protected:
        int64_t *_ptr;
        char *_dataNext;
        DataBlock *_dataBlock;
    };

    FInserter inserter( int64_t from = 0 ) {
        return _count ? FInserter( *this, from ) : FInserter();
    }

    int64_t *lowLevelIndices() { return _indices; }

  private:
    int64_t _count;
    int64_t *_indices;
    char *_data;

    char *_ix( int64_t ix ) {
        ASSERT_LEQ( 0, ix );
        int64_t i = ix == 0 ? 0 :_indices[ ix - 1 ];
        ASSERT_LEQ( 0, i );
        return _data + i;
    }

    const char *_ix( int64_t ix ) const {
        return const_cast< const char * >( const_cast< DataBlock * >( this )->_ix( ix ) );
    }
};

struct StateFlags {

    StateFlags() : flagCount( 0 ), flagMasks( nullptr ) { }

    StateFlags( int32_t count, char *map, char *flags ) :
        flagCount( count ),
        flagMap( flagCount, map ),
        flagMasks( reinterpret_cast< uint64_t * >( flags ) )
    { }

    struct Map {
        Map( const StateFlags *self ) : self( self ) { }
        const StateFlags *self;

        std::string operator[]( int intflag ) const {
            return std::string( self->flagMap[ intflag ], self->flagMap.size( intflag ) );
        }

        int operator[]( std::string flagname ) const {
            for ( int i = 0; i < self->flagCount; ++i )
                if ( (*this)[ i ] == flagname )
                    return i;
            return -1;
        }
    };

    // translation flag numbers <-> flag names
    Map map() const { return Map( this ); }

    std::vector< std::string > flagNames() const {
        std::vector< std::string > out;
        for ( int i = 0; i < flagCount; ++i )
            out.emplace_back( flagMap[ i ], flagMap.size( i ) );
        return out;
    }

    bool hasFlag( int64_t state, int flag ) const {
        return (flagMasks[ state ] & (1 << flag)) != 0;
    }

    bool hasFlag( int64_t state, std::string flagname ) const {
        return hasFlag( state, map()[ flagname ] );
    }

    uint64_t operator[]( int64_t state ) const {
        return flagMasks[ state ];
    }

    // obtain flag numers for state, SmallVector used for optimization
    brick::data::SmallVector< int > listFlags( int64_t state ) {
        uint64_t flags = flagMasks[ state ];
        brick::data::SmallVector< int > out;
        for ( int i = 0; i < flagCount; ++i )
            if ( (flags & (1 << i)) != 0 )
                out.emplace_back( i );
        return out;
    }

    std::vector< std::string > listFlagsStr( int64_t state ) {
        std::vector< std::string > out;
        for ( auto f : listFlags( state ) )
            out.emplace_back( map()[ f ] );
        return out;
    }

    // low-level interface
    int64_t flagCount;
    DataBlock flagMap;
    uint64_t *flagMasks;
};

// Explicit V1/V2 runtime representation
struct Explicit {

    enum class OpenMode { Read, Write };

    Header *header;
    DataBlock forward;
    DataBlock backward;
    DataBlock nodes;
    StateFlags stateFlags;
    brick::mmap::MMap map;

    Explicit() = default;

    Explicit( std::string path, OpenMode mode = OpenMode::Read ) {
        open( path, mode );
    }

    void open( std::string path, OpenMode = OpenMode::Read );
    void finishOpen();

    bool valid() { return static_cast< bool >( header ); }
};

struct PrealocateHelper {
    int fd;
    int64_t _edges;
    int64_t _nodes;
    int64_t _nodeDataSize;
    int32_t _labelSize;
    int32_t _flagCount;
    int32_t _flagStrings;
    Capabilities _capabilities;
    std::string _generator;

    PrealocateHelper( const std::string &path );

    Explicit operator()();

    PrealocateHelper &forward() {
        _capabilities |= Capability::ForwardEdges;
        return *this;
    }

    PrealocateHelper &backward() {
        _capabilities |= Capability::BackwardEdges;
        return *this;
    }

    PrealocateHelper &generator( std::string generator ) {
        _generator = std::move( generator );
        return *this;
    }

    template< typename Label >
    PrealocateHelper &labelSize( Label ) {
        ASSERT_EQ( _labelSize, 0 );
        _labelSize = std::is_empty< Label >::value ? 0 : sizeof( Label );
        return *this;
    }

    PrealocateHelper &uint64Labels() {
        _capabilities |= Capability::UInt64Labels;
        return *this;
    }

    PrealocateHelper &probability() {
        _capabilities |= Capability::Probability;
        return *this;
    }

    PrealocateHelper &edges( int64_t edges ) {
        ASSERT_EQ( _edges, 0 );
        _edges = edges;
        return *this;
    }

    PrealocateHelper &nodes( int64_t nodes ) {
        ASSERT_EQ( _nodes, 0 );
        _nodes = nodes;
        return *this;
    }

    PrealocateHelper &saveNodes( int64_t nodesSize ) {
        ASSERT_EQ( _nodeDataSize, 0 );
        _nodeDataSize = nodesSize;
        _capabilities |= Capability::Nodes;
        return *this;
    }

    PrealocateHelper &saveFlags( int flagCount, int flagStringsSize ) {
        ASSERT_EQ( _flagCount, 0 );
        ASSERT_LEQ( flagCount, 64 );
        _flagCount = flagCount;
        _flagStrings = flagStringsSize;
        _capabilities |= Capability::StateFlags;
        return *this;
    }
};

static inline PrealocateHelper preallocate( const std::string &path ) {
    return PrealocateHelper( path );
}

}
}

namespace divine_test {
namespace dess {

using divine::dess::DataBlock;

struct TestDataBlock {
    TEST(empty) {
        DataBlock empty;
    }

    /* this was dropped from code as it was not used
    TEST(inserterT) {
        char *data = new char[ 100 * sizeof( int64_t ) + 100 * 100 ];
        DataBlock block( 100, data );

        auto inserter = block.inserter< int64_t >();
        for ( int i = 0; i < 100; ++i )
            ASSERT_EQ( inserter.emplace( i ), i );
        for ( int i = 0; i < 100; ++i )
            ASSERT_EQ( block.get< int64_t >( i ), i );
        for ( int64_t i = 0; i < 100; ++i )
            block.map( i )( [ i ]( char *data, int64_t size ) -> void {
                ASSERT_EQ( int64_t( sizeof( int64_t ) ), size );
                ASSERT_EQ( *reinterpret_cast< int64_t *>( data ), i );
            } );
    } */

    TEST(inserter) {
        char *data = new char[ 100 * sizeof( int64_t ) + 100 * 100 ];
        DataBlock block( 100, data );

        auto inserter UNUSED = block.inserter();
        for ( int i = 0; i < 100; ++i )
            ASSERT_EQ( inserter.emplace( std::max( size_t( i ), sizeof( int64_t ) ),
                [ i ]( char *data, int64_t ) -> int64_t {
                    *reinterpret_cast< int64_t * >( data ) = i;
                    return *reinterpret_cast< int64_t * >( data );
                } ), i );
        for ( int i = 0; i < 100; ++i )
            ASSERT_EQ( block.get< int64_t >( i ), i );
        for ( int64_t i = 0; i < 100; ++i )
            block.map( i )( [ i ]( char *data, int64_t size ) -> void {
                ASSERT_EQ( std::max( int64_t( i ), int64_t( sizeof( int64_t ) ) ), size );
                ASSERT_EQ( *reinterpret_cast< int64_t *>( data ), i );
            } );
    }
};

}
}

#endif // DIVINE_COMPACT_COMPACT_H
#endif