from_l2.cpp

vxworks的系统故障诊断项目

                if(!parse_enums(has_debug_info)) return false;
                continue;
            case VARIABLES:
                if(!parse_variables(has_debug_info)) return false;
                continue;
            case PROPOSITIONS:
                if(!parse_propositions(has_debug_info)) return false;
                continue;
            case CLAUSES:
                if(!parse_clauses(has_debug_info)) return false;
                continue;
            case TRANSITIONS:
                if(!parse_transitions(has_debug_info)) return false;
                continue;
            case OBSERVED:
                if(!parse_observed(has_debug_info)) return false;
                continue;
            case COMMANDS:
                if(!parse_commands(has_debug_info)) return false;
                continue;
            case MODES:
                if(!parse_modes(has_debug_info)) return false;
                continue;
            case BACKGROUND:
                if(!parse_background(has_debug_info)) return false;
                continue;
            case INITIAL:
                if(!parse_initial(has_debug_info)) return false;
                continue;
            case NO_SECTION:
                print_parse_error();
                tostream(_STD_ cerr << "Unknown section name `" << linep
			 << "'\n");
                return false;
        }
        assert(0); // can't get here!
    }
    return true;
}


/***************************************************************************
        enums section
 ***************************************************************************/

bool from_l2::parse_enums(bool has_debug_info) {
    // check prereqs
    // no prereqs for enums

    // check we haven't already parsed
    if(!check_parsed( was_enums_parsed(), false, "enums"))
        return false;
    didEnums_ = true;

    // first line: count of number of enumerations
    readline();
    int count = read_integer("number of enumerations");
    if(count<0) return false;
    verbose(_STD_ cout << "\n* Reading " << count << " enumerations\n");


    // create the array
    dest()->allocEnums(count, has_debug_info);

    // successive lines:
    // (1) read the line
    // (2) read the number of members
    // (3) if we don't have debug info:
    //        we're done, create the enum and store it in the array
    //     if we do:
    //        a) read the enum name
    //        b) read the members
    //        c) create & store the dbg_enum
    // if the line doesn't parse, stop and return false
    for(size_t enum_index = 0; enum_index < nenums(); enum_index++) {
        if(!readline()) return false;

        // number of members
        int nmembers = read_integer("number of enumeration members");
        if(nmembers<0) return false;

#ifdef ENABLE_L2_DEBUG_SECTIONS
	if(has_debug_info) {
            char buffer[MBA_MAX_LINE_SIZE];
            MBA_string enum_name;
            MBA_string *enum_member_names;
            enum_member_names = new MBA_string [nmembers];

            // read enumeration name
            if(!skip_word_boundary()) {
                tostream(_STD_ cerr << "Missing debug info for enumeration "
			<< enum_index << _STD_ endl);
                return false;
            }
            str_get_next_word(buffer, index, line);
            enum_name = buffer;

            // read the members
            for(int i=0; i<nmembers; i++) {
                if(!skip_word_boundary()) {
                    tostream(_STD_ cerr << "Missing " << (nmembers-i)
			     << " enumeration names\n");
                    return false;
                }
                str_get_next_word(buffer, index, line);
                enum_member_names[i] = buffer;
            }

            dest()->setEnum(enum_index, new dbg_L2rEnumeration(
                    enum_index, nmembers,
                    enum_name, enum_member_names));
            delete [] enum_member_names;
        } else
#endif
	{
	    // no debug info
            dest()->setEnum(enum_index, new L2rEnumeration(enum_index, nmembers));
        }

#ifdef WITH_OSTREAM
        // debug print
        verbose(getEnum(enum_index)->toOStream_long(_STD_ cout));
#endif
    }
    return true;
}



/***************************************************************************
        variables section
 ***************************************************************************/

bool from_l2::parse_variables(bool has_debug_info) {
    // check prereqs
    if(!check_parsed( was_enums_parsed(), true, "enums"))
        return false;

    // check we haven't already parsed
    if(!check_parsed( was_variables_parsed(), false, "variables"))
        return false;
    didVariables_ = true;

    // first line: count of number of variables
    readline();
    int count = read_integer("number of variables");
    if(count<0) return false;
    verbose(_STD_ cout<< "\n* Reading " << count << " variables\n");
    dest()->allocVars(count, has_debug_info);

    // read n variables
    for(size_t var_index = 0; var_index < nvars(); var_index++) {
        if(!readline()) return false;
        int enumID = read_integer("enum ID");
        if(enumID<0) return false;

        const L2rEnumeration *the_enum = getEnum(enumID);
        if(!the_enum) return false;

        L2rVariable *retval;

#ifdef ENABLE_L2_DEBUG_SECTIONS
        if(has_debug_info) {
            // read the fully-qualified variable name
            char varname[MBA_MAX_LINE_SIZE];
            skip_word_boundary();
            str_get_next_word(varname, index, line);

            retval = new dbg_L2rVariable(var_index, the_enum, varname);
	} else
#endif
	{
	    // we're done; store in the array
	    retval = new L2rVariable(var_index, the_enum);
	}
        dest()->setVar(var_index, retval);

#ifdef WITH_OSTREAM
        // debug output
        verbose(retval->toOStream_long(_STD_ cout));
#endif
    }
    return true;
}

/***************************************************************************
        propositions section
 ***************************************************************************/

bool from_l2::parse_one_prop(unsigned prop_index,
        bool equality, bool positive) {
    int varID, valOrVarID;
    if(!readline()) return false;

    if(!skip_word_boundary()) return false;
    varID = read_integer("variable ID");
    if(varID < 0) return false;

    if(!skip_word_boundary()) return false;
    valOrVarID = read_integer("value");
    if(valOrVarID < 0) return false;

    // check the variable ID is valid
    const L2rVariable *the_var = getVar(varID);
    if(!the_var) return false;

    L2rProposition *the_prop;

    if(!equality) {
        // check that the memberID is a valid ID for the variable type.
        const L2rEnumeration *the_enum = the_var->type();
        if(!the_enum->isValidMember(valOrVarID)) return false;

        // we're safe; create & store
        the_prop =new L2rPropVarValue(prop_index,
                the_var, positive, valOrVarID);
    } else {
        // check the varID is valid
        const L2rVariable *other_var = getVar(valOrVarID);
        if(!other_var) return false;
        if(the_var->type() != other_var->type()) {
            tostream(_STD_ cerr <<"Type mismatch (`"
                    << the_var->type() << "' and `" << other_var->type()
                    << "') in `" << the_var << (positive?"=":"!=") << other_var
                    << "'\n");
            return false;
        }
        the_prop = new L2rPropVarVar(prop_index,
                the_var, positive, other_var);
    }
    dest()->setProp(prop_index, the_prop);
    verbose(the_prop->toOStream_long(_STD_ cout));
    return true;
}


bool from_l2::parse_propositions(bool /*has_debug_info*/) {
    // check prereqs
    if(!check_parsed( was_enums_parsed(), true, "enums"))
        return false;
    if(!check_parsed( was_variables_parsed(), true, "variables"))
        return false;

    // check we haven't already parsed
    if(!check_parsed( was_propositions_parsed(), false, "propositions"))
        return false;
    didPropositions_ = true;


    // first line: count of number of positive props
    readline();
    // counts:
    int pos_count, neg_count, same_count, diff_count;

    pos_count = read_integer("number of positive propositions");
    if(pos_count<0) return false;
    if(!skip_word_boundary()) return false;

    neg_count = read_integer("number of negative propositions");
    if(neg_count<0) return false;
    if(!skip_word_boundary()) return false;

    same_count = read_integer("number of equalities");
    if(same_count<0) return false;
    if(!skip_word_boundary()) return false;

    diff_count = read_integer("number of inequalities");
    if(diff_count<0) return false;
    // nothing more to read; don't s_w_b

    // allocate all the propositions
    dest()->allocProps(pos_count + neg_count + same_count + diff_count);
    verbose(_STD_ cout
            << "\n* Reading " << nprops() << " propositions ("
            << pos_count  << " positive, "
            << neg_count  << " negative,\n          "
            << same_count << " equalities, "
            << diff_count << " inequalities)\n");

    unsigned prop_id=0;
    int i; // signed b/c the counts are

    for(i=0 ; i < pos_count; ++i, ++prop_id)
        // not an equality; positive
        if(!parse_one_prop(prop_id, false, true)) return false;

    for(i=0 ; i < neg_count; ++i, ++prop_id)
        // not an equality; negative
        if(!parse_one_prop(prop_id, false, false)) return false;

    for(i=0 ; i < same_count; ++i, ++prop_id)
        // equality; positive
        if(!parse_one_prop(prop_id, true, true)) return false;

    for(i=0 ; i < diff_count; ++i, ++prop_id)
        // equality; negative
        if(!parse_one_prop(prop_id, true, false)) return false;

    return true;
}

/***************************************************************************
        clauses section
 ***************************************************************************/

bool from_l2::parse_clauses(bool has_debug_info) {
    // check prereqs
    if(!check_parsed( was_propositions_parsed(), true, "propositions"))
        return false;

    // check we haven't already parsed
    if(!check_parsed( was_clauses_parsed(), false, "clauses"))
        return false;
    didClauses_ = true;

    // first line: count of number of clauses
    readline();
    int count = read_integer("number of clauses");
    if(count<0) return false;
    verbose(_STD_ cout<< "\n* Reading " << count << " clauses\n");

    dest()->allocClauses(count, has_debug_info);

    // read n clauses
    for(size_t clause_index = 0; clause_index < nclauses(); clause_index++) {
        if(!readline()) return false;

#ifdef ENABLE_L2_DEBUG_SECTIONS
        // if we have debug info, read the name first
        char component[MBA_MAX_LINE_SIZE];
        if(has_debug_info) {
            str_get_next_word(component, index, line);
            if(!skip_word_boundary()) return false;
        }
        unsigned first_prop_index = index;
#else
        unsigned first_prop_index = 0;
#endif

        // two passes: first:  count and allocate an array big enough;
        //             second: fill the array

        // first, count the number of props; note: not an error
        // to hit end-of-line -- in fact, we expect to!
        unsigned nclause_props = 0;
        while(skip_word_boundary(false)) {
            if(0>read_integer("prop ID")) return false;
            nclause_props++;
        }

        // go to the beginning of the line (except for the component name)
        index = first_prop_index;

        const L2rProposition **clause_props =
            L2_alloc_array(const L2rProposition* , nclause_props);

        for(unsigned i=0; i<nclause_props; i++) {
            // now it _is_ an error, since we have counted already
            if(!skip_word_boundary(true)) return false;
            int propID = read_integer("prop ID");
            if(propID<0) return false;
            const L2rProposition *the_prop = getProp(propID);
            if(!the_prop) return false;
            clause_props[i] = the_prop;
        }

        // create the clause object; no need to copy the props
        L2rClause *cls;