SymbolicDiagnose.cc

Go to the documentation of this file.

#include<iostream>
#include<string>
#include<vector>
#include<regex>
#include <fstream>
#include<boost/program_options.hpp>
#include<diades/automata/ObservableComponent.hh>
#include<diades/automata/Event.hh>
#include<diades/automata/experimental/Algorithms.hh>
#include<diades/automata/experimental/LocalCandidateStateMachine.hh>
#include<diades/sdmdl/experimental/StateInfoEncoder.hh>
#include<diades/sdmdl/Variable.hh>
#include<diades/sdmdl/experimental/EventEncoder.hh>
#include<diades/sdmdl/experimental/BddStateMachine.hh>
#include<diades/sdmdl/experimental/BddStateMachineEncoding.hh>
#include<diades/sdmdl/experimental/FormulaUtils.hh>

using std::cout;
using std::string;
using std::vector;
using Diades::Automata::ObservableComponent;
using Diades::Automata::Event;
using Diades::Sdmdl::Experimental::BddStateMachine;
using Diades::Sdmdl::Experimental::Assignment;
using Diades::Sdmdl::Experimental::EventEncoder;
using Diades::Sdmdl::Experimental::StateInfoEncoder;
using Diades::Sdmdl::VariableFactory;
using Diades::Sdmdl::Variable;
using Diades::Sdmdl::FormulaVector;



namespace Poptions = boost::program_options;
namespace Lcm = Diades::Automata::Experimental::LocalCandidateMachine;

const string program("dd-symb-diagnose");

void initialiseOptions(int argc, char * argv[],
        Poptions::options_description & desc,
        Poptions::options_description & visible,
        Poptions::variables_map & vm) {
    visible.add_options()
            ("help", "produce help message")
            ("scenario", Poptions::value< string >(), "scenario file (evts format), mandatory");

    Poptions::options_description hidden("Hidden options");
    hidden.add_options()
            ("model-file", Poptions::value< vector<string> >(), "model file (des_comp format)");
    Poptions::positional_options_description p;
    p.add("model-file", -1);
    desc.add(visible).add(hidden);
    Poptions::store(Poptions::command_line_parser(argc, argv).
            options(desc).positional(p).run(), vm);
    Poptions::notify(vm);
}

void printErrorCmdLine(const string & msg, Poptions::options_description & visible) {
    cout << msg << '\n';
    cout << "Command line error: here is the usage\n"
            << program << " [model.des_comp]\n" << visible << '\n';
    exit(0);
}

void printError(const string & msg) {
    cout << msg << '\n';
    exit(0);
}

void analyseOptions(Poptions::variables_map & vm,
        Poptions::options_description & visible,
        vector<string> & models,
        vector<string> & scenarios) {
    if (vm.count("help")) {
        cout << "Usage: " << program << " [model.des_comp]\n"
                << visible << "\n";
        exit(0);
    }
    if (!vm.count("model-file")) {
        printErrorCmdLine("A model file is missing.", visible);
    }
    auto & modelNames = vm["model-file"].as<vector < string >> ();
    if (modelNames.size() > 1) {
        printError("Only one model file is allowed.");
    }
    if (!vm.count("scenario")) {
        printErrorCmdLine("A scenario file is missing", visible);
    }

    std::regex desCompSuffix("[a-zA-Z_][a-zA-Z_0-9]*\\.des_comp");
    if (!std::regex_match(modelNames[0], desCompSuffix)) {
        printError("Expecting a model file with a name ending with .des_comp");
    }

    auto & scenarioName = vm["scenario"].as<string>();
    std::regex evtsSuffix("[a-zA-Z_][a-zA-Z_0-9]*\\.evts");
    if (!std::regex_match(scenarioName, evtsSuffix)) {
        printError("Expecting a scenario file with a name ending with .evts");
    }
    models.push_back(modelNames[0]);
    scenarios.push_back(scenarioName);
}

bool loadModels(const vector<string> & modelNames,
        vector<ObservableComponent> & models) {
    bool result = true;
    size_t index = 0;
    while (result && (index < modelNames.size())) {
        models.push_back(ObservableComponent());
        result = models.back().import(modelNames[index]);
        ++index;
    }
    return result;
}

bool loadScenario(const string & scenarioFile, vector<Event> & observations,
        const vector<ObservableComponent> & models) {
    ifstream file(scenarioFile);
    bool result = file.is_open();
    if (result) {
        while (result && file) {
            string label;
            file >> label;
            if (!label.empty()) {
                observations.push_back(Event::getEvent(label));
                result = models[0].containsEvent(observations.back());
            }
        }
        file.close();
    }
    return result;

}

void printSolution(const BddStateMachine::SlEvents & solution,
                   StateInfoEncoder & stateEncoder,
                   Lcm::CandidateManager & candManager,
                   Lcm::EvSetManager & setManager,
                   Lcm::LocalStateInfoManager & locStateInfoManager,
                   Lcm::EvManager & manager) {
    std::list< std::list<Assignment> > listSolutions;
    exportToDisjunctiveNormalForm(solution, listSolutions);

    std::cout << "Here is the solution:" << std::endl;
    size_t counter = 0;
    // listSolutions is a list (disjunction) of conjunction of Assignments: such a conjunction is candidate
    for (auto & candidate : listSolutions) {
        // a candidate is a list (conjunction) of Assignments
        std::cout << "Candidate " << counter++ << ": {";
        for (auto & fault : candidate) {
            // first I get the CandidateId associated with the Value of the Variable in the Assignement 'fault'
            // This CandidateId is the StateInfoId of the CandidateManager (i.e. a StateInfoManager<Candidate>)
            // I retrieve the StateInfoId from the stateEncoder.
            Lcm::CandidateId candId = stateEncoder.getStateInfoId(fault).first;

            // Then I can get the corresponding Candidate associated with candId.first
            // This Candidate is stored in the CandidateManager=StateInfoManager<Candidate>
            const Lcm::Candidate & faultCandidate = candManager.getStateProperty(candId);


            // A Candidate is actually in Lcm a  LocalCandidate<LocalStateInfoId,EvSet>
            // So I can get the LocalStateInfoId of the Candidate and its EvSet
            auto & state = faultCandidate.state();
            auto & faults = faultCandidate.faults();

            // From the EvSet I can get back a vector of Lcm::Event thanks to the EventSetManager
            vector<Lcm::EventInfoId> faultEvents = setManager.decodeEventSet(faults);
                
            // From the LocalStateInfoId I can get the LocalStateInfo = StateInfoStringLabel
            // that is the actual information about a state of the component
            std::cout << "state = " << locStateInfoManager.getStateProperty(state) << " ";


            // From a vector of Lcm::Event I can get the label of the event thanks to the EventManager
            std::cout << "faults = ";
            for (auto evt : faultEvents) {
                std::cout << evt << "<->" << manager.getEvent(evt) << " ";
            }
            // DONE !
        }
        std::cout << "}\n";
    }
}

void runGlobalDiagnosisProblem(const ObservableComponent & component,
        const vector<Event> & observations) {
    Lcm::EvManager manager;
    Lcm::EvSetManager setManager;
    Lcm::LocalStateInfoManager locStateInfoManager;
    Lcm::CandidateManager candManager;
    Lcm::Fsm result;
    transformToCandidateStateMachine(component,
            manager,
            setManager,
            locStateInfoManager,
            candManager,
            result);

    vector<Lcm::EventInfoId> observables;
    vector<Lcm::EventInfoId> nonObservables;


    // dealing with observables/non observables
    for (auto & e : component.events()) {
        if (component.mask().isIdentifiable(e)) {
            observables.push_back(manager.eventId(e.label()));
        } else {
            nonObservables.push_back(manager.eventId(e.label()));
        }
    }


    // result contains a Lcm::Fsm, let us convert to a BddStateMachine 
    // First I need a VariableFactory to get Variables
    VariableFactory varFactory;

    // Then an EventEncoder to create the Variable that encodes events
    EventEncoder evtEncoder(varFactory);
    EventEncoder::VariableEncoderId varEventId = evtEncoder.encodeEventRange(result.eventBegin(), result.eventEnd());
    Variable & eventVar = evtEncoder.getVariable(varEventId);


    // Then a StateInfoEncoder is required to encode stateVar
    StateInfoEncoder stateEncoder(varFactory);
    StateInfoEncoder::VariableEncoderId varStateId = stateEncoder.encodeStateInfoRange(result.statePropertyIdBegin(), result.statePropertyIdEnd());
    Variable & stateVar = stateEncoder.getVariable(varStateId);

    // and a nextStateVar is also required
    StateInfoEncoder::VariableEncoderId nextVarStateId = stateEncoder.encodeStateInfoRange(result.statePropertyIdBegin(), result.statePropertyIdEnd());
    Variable & nextStateVar = stateEncoder.getVariable(nextVarStateId);

    BddStateMachine bddMachine;
    encode(result, stateVar, nextStateVar, eventVar, bddMachine);

    FormulaVector nonObservable;
    nonObservable.push_back(bddMachine.factory().isFalse());
    for (auto & evt : nonObservables) {
        stringstream evtText;
        evtText << evt;
        auto & value = eventVar.getValue(evtText.str());
        auto & nonObs = nonObservable[0].get();
        nonObservable.clear();
        nonObservable.push_back(nonObs || bddMachine.event(value));
    }
    auto & nonObs = nonObservable[0].get();
    stringstream stream;
    stream << result.getStatePropertyId(*result.initialStateBegin());
    string initialStateIdText = stream.str();
    FormulaVector currentStates;
    currentStates.push_back(bddMachine.sources(stateVar.getValue(initialStateIdText)));

    for (auto & e : observations) {
        Lcm::EventInfoId evt = manager.eventId(e.label());
        stringstream evtText;
        evtText << evt;
        auto & value = eventVar.getValue(evtText.str());
        auto & obs = bddMachine.event(value);
        auto & currentBeliefState = currentStates[0].get();
        currentStates.clear();
        currentStates.push_back(bddMachine.reach(currentBeliefState, nonObs, obs));
    }

    printSolution(currentStates[0].get(),stateEncoder,candManager,setManager,locStateInfoManager,manager);
}



int main(int argc, char * argv[]) {

    Poptions::options_description desc("Complete options");
    Poptions::options_description visible("Allowed options");
    Poptions::variables_map vm;
    initialiseOptions(argc, argv, desc, visible, vm);
    // 1 model and 1 scenario for now but anyway...
    vector<string> modelNames;
    vector<string> scenarios;
    analyseOptions(vm, visible, modelNames, scenarios);

    vector<ObservableComponent> models;
    if (!loadModels(modelNames, models)) {
        printError("Cannot read the models from the given files");
    }

    for (auto & scenario : scenarios) {
        vector<Event> observations;
        if (!loadScenario(scenario, observations, models)) {
            printError("Cannot read a scenario from the given files");
        }
        runGlobalDiagnosisProblem(models[0], observations);
    }
    return 0;
}