reader.h

// -*- C++ -*- (c) 2010-2011 Jan Kriho <[email protected]>

#ifndef DIVINE_READER_H
#define DIVINE_READER_H


#include <wibble/test.h>
#include <fstream>
#include <list>
#include <vector>
#include <string.h>
#include <divine/pma/format.h>

namespace divine {
namespace pma {


template< typename N >
struct Reader {
    std::fstream *infile;
    fileHeader header;
    architectureInfo archinfo;

    std::string getStateDesc(tableDescriptor td, nodeIndexItem node, bool seekg = true) {
        if (seekg) {
            infile->seekg(td.offset + td.nodeCount*NODE_INDEX_ITEM_SIZE + node.dataOffset + td.succsCount*NODE_DESCRIPTOR_SIZE + node.nodeSize);
        }
        std::string stateDesc;
        stateDesc.resize(node.descSize, '\0');
        char * array;
        array = new char[node.descSize];
        infile->read(array, node.descSize - 1);
        array[node.descSize - 1] = '\0';
        stateDesc.insert(0, array, node.descSize);
        return stateDesc;
    }

    std::vector< nodeDescriptor > getSuccessors(tableDescriptor td, nodeIndexItem node, bool seekg = true) {
        if (seekg) {
            infile->seekg(td.offset + td.nodeCount*NODE_INDEX_ITEM_SIZE + node.succsOffset);
        }

        std::vector< nodeDescriptor > successors;
        successors.resize(node.successors);
        if (node.successors > 0) {
            N * array = new N (node.successors * NODE_DESCRIPTOR_SIZE);
            infile->read(array->data(), node.successors * NODE_DESCRIPTOR_SIZE);

            int offset = 0;

            for (int i = 0; i < node.successors; i++) {
                offset = successors[i].template read(*array, offset);
            }

            array->free();

            delete array;
        }

        return successors;
    }

    nodeDescriptor getSucc() { //private use only
        return getInitial(0, false); // use existing infrastructure w/o seeking
    }

    std::vector< nodeIndexItem > getNodeIndex(tableDescriptor td, bool seekg = true) {
        if (seekg) {
            std::cerr << "Seeking to " << td.offset << std::endl;
            infile->seekg(td.offset);
        }
        std::vector< nodeIndexItem > ni;
        ni.resize(td.nodeCount);
        for (int i = 0; i < td.nodeCount; i++) {
            ni[i] = getNodeIndexItem();
        }
        return ni;
    }

    nodeIndexItem getNodeIndexItem(int64_t offset_to = 0, bool seekg = false) {
        if (seekg) {
            infile->seekg(offset_to);
        }
        N array(NODE_INDEX_ITEM_SIZE);
        int offset = 0;

        infile->read(array.data(), NODE_INDEX_ITEM_SIZE);

        nodeIndexItem nii;

        nii.template read< N >(array, 0);

        array.free();

        return nii;
    }

    std::vector< tableDescriptor > getTableDescriptors(bool seekg = true) {
        if( seekg ) {
            infile->seekg(TOTAL_HEADER_SIZE + header.initials * NODE_DESCRIPTOR_SIZE);
        }
        std::vector< tableDescriptor > tds;
        tds.resize(getTableCount());
        for (int i = 0; i < getTableCount(); i++) {
            tds[i] = getTableDesc();
        }
        return tds;
    }

    tableDescriptor getTableDesc(int id = 0, bool seekg = false) {
        if (seekg) {
            infile->seekg(TOTAL_HEADER_SIZE +
                           header.initials * NODE_DESCRIPTOR_SIZE +
                           id * TABLE_DESCRIPTOR_SIZE);
        }
        N array(TABLE_DESCRIPTOR_SIZE);
        int offset = 0;

        infile->read(array.data(), TABLE_DESCRIPTOR_SIZE);

        tableDescriptor td;

        td.template read<N>(array, 0);
        /*
        td.offset = le64toh((*(int64_t *)(array + offset)));
                offset += sizeof(td.offset);
        td.nodeCount = le64toh((*(int64_t *)(array + offset)));
                offset += sizeof(td.offset);
        td.succsCount = le64toh((*(int64_t *)(array + offset)));
                offset += sizeof(td.succsCount);
        td.dataSize = le64toh((*(int64_t *)(array + offset)));
                offset += sizeof(td.offset);

        assert(offset == TABLE_DESCRIPTOR_SIZE);
        */
        return td;
    }

    int getTableCount() {
        switch (header.vertexDistribution) {
            case None:
                return 1;
                break;
            case Hash:
                return header.mpiWorkers * header.localWorkers;
        }
    }

    std::vector< nodeDescriptor > getInitials(bool seekg = true) {
        std::vector< nodeDescriptor > initials;
        initials.resize( header.initials );
        for (int i = 0; i < header.initials; i++) {
            initials[i] = getInitial(i, (i == 0 ? seekg : false) );
        }
        return initials;
    }

    nodeDescriptor getInitial(int id, bool seekg = true) {
        if ( seekg ) {
            infile->seekg(TOTAL_HEADER_SIZE + NODE_DESCRIPTOR_SIZE * id, std::ios::beg);
        }
        N array(NODE_DESCRIPTOR_SIZE);
        int offset = 0;

        infile->read(array.data(), NODE_DESCRIPTOR_SIZE);

        nodeDescriptor initial;

        initial.template read<N>(array, 0);
        /*
        initial.nodeNo = le64toh((*(int64_t *)((array) + offset)));
                offset += sizeof(initial.nodeNo);
        initial.table = le32toh((*(int32_t *)((array) + offset)));
                offset += sizeof(initial.table);

        assert(offset == NODE_DESCRIPTOR_SIZE);*/

        return initial;

    }

    fileHeader getHeader() {
        return header;
    }

    architectureInfo getArchInfo() {
        return archinfo;
    }

    bool readHeader() {
        infile->seekg(0, std::ios::beg);
        N array(TOTAL_HEADER_SIZE);
        int offset = 0;

        /*int count = infile->gcount();
        int pos = infile->tellg();
        */
        infile->read(array.data(), TOTAL_HEADER_SIZE);
        /*
        count = infile->gcount();
        pos = infile->tellg();
        */

        offset = header.template read<N>(array, offset);
        offset = archinfo.template read<N>(array, offset);

        assert(offset == TOTAL_HEADER_SIZE);

        if (header.header == 666) {
            return true;
        }
        else {
            return false;
        }
    }


    Reader( std::string &filename ) {
        infile = new std::fstream(filename.c_str(), std::ios::in | std::ios::binary );
        if (!readHeader()) {
            std::cerr << "Not a valid state space dump!" << std::endl;
            exit( 1 );
        }
    }

    ~Reader() {
        if (infile) {
 //           delete infile;
        }
    }

};

}
}