CPSolutionObserver.cpp

Go to the documentation of this file.

#ifdef USE_CP
 
#include "CPSolutionObserver.h"
#include "model/bpmnos/src/DecisionTask.h"
#include "model/bpmnos/src/SequentialAdHocSubProcess.h"
#include "model/bpmnos/src/extensionElements/MessageDefinition.h"
#include "model/bpmnos/src/extensionElements/Timer.h"
#include "execution/engine/src/Engine.h"
#include "execution/engine/src/SequentialPerformerUpdate.h"
#include <iostream>
 
using namespace BPMNOS::Execution;
 
CPSolutionObserver::CPSolutionObserver(const CPModel* cp)
 : cp(cp)
 , flattenedGraph( cp->flattenedGraph )
 , _solution( cp->getModel() )
 , lastPosition(0)
{
  // add evaluators for lookup tables
  for ( auto& lookupTable : cp->scenario->model->lookupTables ) {
    _solution.addEvaluator( 
      lookupTable->name,
      [&lookupTable](const std::vector<double>& operands) -> double {
        return lookupTable->at(operands);
      }
    );
  }
  
  std::vector<double> positions;
  positions.resize( flattenedGraph->vertices.size() );
  std::iota(positions.begin(), positions.end(), 1);
  initializePositions(positions);
}
 
void CPSolutionObserver::subscribe(Engine* engine) {
  lastPosition = 0;
  engine->addSubscriber(this, 
    Execution::Observable::Type::Event,
    Execution::Observable::Type::Token
  );
}
 
void CPSolutionObserver::unsubscribe(Engine* engine) {
  engine->removeSubscriber(this, 
    Execution::Observable::Type::Event,
    Execution::Observable::Type::Token
  );
}
 
void CPSolutionObserver::notice(const Observable* observable) {
  if ( observable->getObservableType() == Execution::Observable::Type::Token ) {
    synchronize( static_cast<const Token*>(observable) );
  }
  else {
    assert( observable->getObservableType() == Execution::Observable::Type::Event );
    synchronize( static_cast<const Event*>(observable) );
  }
}
 
void CPSolutionObserver::synchronize(const Token* token) {
//std::cerr << "Token: " << token->jsonify() << std::endl;
  if (
    token->state == Token::State::CREATED || 
    token->state == Token::State::ARRIVED || 
    token->state == Token::State::READY || 
    token->state == Token::State::BUSY ||
    token->state == Token::State::DEPARTED ||
    token->state == Token::State::WAITING ||
    token->state == Token::State::FAILING ||
    token->state == Token::State::FAILED
  ) {
    return;
  }
  
  auto vertex = flattenedGraph->getVertex(token);
  if ( !vertex ) {
    // a token may enter the start event of an event-subprocess that cannot be triggered
    // such a token will be withdrawn and no vertex exists 
    return;
  }
 
//std::cerr << lastPosition << " - Synchronise: " << token->jsonify() << std::endl;
  if ( token->state == Token::State::ENTERED ) {
    if ( 
      vertex->node->represents<BPMN::TypedStartEvent>() ||
      ( vertex->node->represents<BPMN::CatchEvent>() && vertex->inflows.front().second->node->represents<BPMN::EventBasedGateway>() )
    ) {
      // vertex enters a node that is either a typed start event or one alternative following an event-based gateway
      // typed start event and alternatives following an event-based gateway are considered when triggered
      return;
    }
 
    // entry at node
 
    // set position
    finalizePosition( vertex );
 
    // set visit, status, data, globals
    _solution.setVariableValue( cp->visit.at(vertex), true );
    synchronizeStatus(token->status,vertex);
    synchronizeData(*token->data,vertex);
    synchronizeGlobals(token->globals,vertex);
 
    if (
      vertex->entry<BPMN::UntypedStartEvent>() ||
      vertex->entry<BPMN::Gateway>() ||
      ( vertex->entry<BPMN::ThrowEvent>() && !vertex->entry<BPMN::SendTask>() )
    ) {
      // vertex is instantaneous
//std::cerr << "clear instantaneous exit: " << token->jsonify() << std::endl;
      finalizePosition(exit(vertex));
      // finalize unvisited subsequent positions
      finalizeUnvisitedSubsequentPositions(exit(vertex));
    }
  }
  else if ( token->node && token->state == Token::State::COMPLETED && token->node->represents<BPMN::TypedStartEvent>() ) {
    // set position
    finalizePosition( entry(vertex) );
    finalizePosition( vertex );
 
    // event-subprocess is triggered
    _solution.setVariableValue( cp->visit.at(vertex), true );
    // for typed start events, operators of event-subprocess are applied before completion
    synchronizeData(*token->data,vertex);
    synchronizeGlobals(token->globals,vertex);
 
    finalizeUnvisitedSubsequentPositions(vertex);
  }
  else if ( token->node && token->state == Token::State::WITHDRAWN && token->node->represents<BPMN::TypedStartEvent>() ) {
    // event-subprocess is not triggered
    setPosition( entry(vertex), ++lastPosition );
    unvisitEntry( entry(vertex) );
    setPosition( vertex, ++lastPosition );
    unvisitExit( vertex );
    finalizeUnvisitedSubsequentPositions(vertex);
//    _solution.setVariableValue( cp->visit.at(vertex), false );
  }
  else if (
    ( !token->node && token->state == Token::State::DONE ) || // Process
    ( token->node && token->state == Token::State::EXITING && !token->node->represents<BPMN::TypedStartEvent>() ) || // Activity
    ( token->node && token->state == Token::State::COMPLETED && token->node->represents<BPMN::CatchEvent>() && !token->node->represents<BPMN::ReceiveTask>() )
  ) {
 
    auto entryVertex = entry(vertex);
    if (
      entryVertex->inflows.size() == 1 &&
      entryVertex->inflows.front().second->node->represents<BPMN::EventBasedGateway>()
    ) {
      assert( vertex->exit<BPMN::CatchEvent>() );
      auto gateway = entryVertex->inflows.front().second;
      setTriggeredEvent( gateway, entryVertex );
      finalizePosition( entryVertex );
      finalizePosition( vertex );
 
      // exit of node
      _solution.setVariableValue( cp->visit.at(vertex), true );
 
      synchronizeStatus(token->status,vertex);
      synchronizeData(*token->data,vertex);
      synchronizeGlobals(token->globals,vertex);
 
      finalizeUnvisitedSubsequentPositions(gateway);
    }
    else {
      // set position
      finalizePosition( vertex );
 
      synchronizeStatus(token->status,vertex);
      synchronizeData(*token->data,vertex);
      synchronizeGlobals(token->globals,vertex);
 
      finalizeUnvisitedSubsequentPositions(vertex);
    }
  }
//std::cerr << "#Token" << std::endl;
}
 
void CPSolutionObserver::synchronize(const Event* event) {
//std::cerr << "Event: " << event->jsonify() << std::endl;
  if ( dynamic_cast<const EntryEvent*>(event) ) {
//std::cerr << "Entry: " << event->jsonify() << std::endl;
    auto vertex = flattenedGraph->getVertex( event->token );
    if ( !flattenedGraph->dummies.contains(vertex) ) {
      auto timestamp = event->token->owner->systemState->getTime();
      setTimestamp(vertex, timestamp );
    }
  }
  else if ( dynamic_cast<const ExitEvent*>(event) ) {
//std::cerr << "Exit: " << event->jsonify() << std::endl;
    auto vertex = flattenedGraph->getVertex( event->token );
    if ( !flattenedGraph->dummies.contains(vertex) ) {
      auto timestamp = event->token->owner->systemState->getTime();
      setTimestamp(vertex, timestamp );
    }
  }
  else if ( auto messageDeliveryEvent = dynamic_cast<const MessageDeliveryEvent*>(event) ) {
//std::cerr << "Message delivery: " << event->jsonify() << std::endl;
    auto vertex = flattenedGraph->getVertex( event->token );
    // set timestamp of message delivery
    auto timestamp = event->token->owner->systemState->getTime();
    if ( vertex->node->represents<BPMN::ReceiveTask>() ) {
      setLocalStatusValue(vertex,BPMNOS::Model::ExtensionElements::Index::Timestamp,timestamp);
    }
    else {
      setTimestamp(vertex,timestamp);
    }
    auto message = messageDeliveryEvent->message.lock();
    assert( message );
    auto senderId = message->header[ BPMNOS::Model::MessageDefinition::Index::Sender ].value();
    assert( flattenedGraph->vertexMap.contains({senderId,{},message->origin}) );
    // TODO: sender must not be within loop
    auto& [senderEntry,senderExit] = flattenedGraph->vertexMap.at({senderId,{},message->origin}); 
    setMessageDeliveryVariableValues(senderEntry,vertex,timestamp);
  }
  else if ( auto choiceEvent = dynamic_cast<const ChoiceEvent*>(event) ) {
//std::cerr << "Choice: " << event->jsonify() << std::endl;
    auto vertex = flattenedGraph->getVertex( event->token );
    // set timestamp of choice
    auto timestamp = event->token->owner->systemState->getTime();
    setLocalStatusValue(vertex,BPMNOS::Model::ExtensionElements::Index::Timestamp,timestamp);
    // apply choices
    auto extensionElements = vertex->node->extensionElements->as<BPMNOS::Model::ExtensionElements>();
    assert( extensionElements );
    assert( extensionElements->choices.size() == choiceEvent->choices.size() );
    for (size_t i = 0; i < extensionElements->choices.size(); i++) {
      auto choice = extensionElements->choices[i].get();
      auto choiceValue = choiceEvent->choices[i];
      setLocalStatusValue(vertex, choice->attribute->index, choiceValue);
      // set discretizer if multipleOf constraint exists
      if ( choice->multipleOf && cp->discretizerMap.contains({vertex, choice->attribute}) ) {
        auto multipleOf = choice->multipleOf->execute(event->token->status, *event->token->data, event->token->globals);
        if ( !multipleOf.has_value() ) {
          throw std::logic_error("CPSolutionObserver: Unable to evaluate multipleOf for choice '" + choice->attribute->id + "'");
        }
        _solution.setVariableValue( cp->discretizerMap.at({vertex, choice->attribute}), (double)(choiceValue / multipleOf.value()) );
      }
    }
  }
//std::cerr << "#Event" << std::endl;
}
 
 
 
void CPSolutionObserver::setMessageDeliveryVariableValues( const Vertex* sender, const Vertex* recipient, BPMNOS::number timestamp ) {
//std::cerr << "Sen:" << sender->jsonify() << std::endl;  
//std::cerr << "Rec:" << recipient->jsonify() << std::endl;  
  for ( auto candidate : sender->recipients ) {
    assert( cp->messageFlow.contains({sender,candidate}) );
//std::cerr << "message_{" << sender->reference() << " -> " << candidate.reference() << "} := " << (&candidate == recipient) << std::endl; 
    _solution.setVariableValue( cp->messageFlow.at({sender,candidate}), (double)(candidate == recipient) );
  }
  for ( auto candidate : recipient->senders ) {
    assert( cp->messageFlow.contains({candidate,recipient}) );
    _solution.setVariableValue( cp->messageFlow.at({candidate,recipient}), (double)(candidate == sender) );
//std::cerr << "message_{" << candidate.reference() << " -> " << recipient->reference() << "} := " << (&candidate == sender) << std::endl; 
  }
  // set message delivery time
  if ( recipient->node->represents<BPMN::ReceiveTask>() || recipient->node->represents<BPMN::MessageStartEvent>() ) {
    setLocalStatusValue( recipient, BPMNOS::Model::ExtensionElements::Index::Timestamp, (double)timestamp );
  }
  else {
    _solution.setVariableValue( cp->status.at(recipient)[BPMNOS::Model::ExtensionElements::Index::Timestamp].value, (double)timestamp );
  }
 
  // set recipient content variables
  auto& recipientContentMap = cp->messageContent.at(recipient);
  auto& senderContentMap = cp->messageContent.at(sender);
  for ( auto& [key, recipientContent ] : recipientContentMap ) {
    assert( senderContentMap.contains(key) );
    auto& senderContent = senderContentMap.at(key);
    CPModel::AttributeEvaluation evaluation(
      _solution.evaluate( senderContent.defined ),
      _solution.evaluate( senderContent.value )
    );
    if ( evaluation ) {
      _solution.setVariableValue( recipientContent.defined, evaluation.defined() );
      _solution.setVariableValue( recipientContent.value, evaluation.value() );
    }
  }
}
 
std::optional< BPMN::Activity::LoopCharacteristics> CPSolutionObserver::getLoopCharacteristics(const Vertex* vertex) const {
  auto activity = vertex->node->represents<BPMN::Activity>();
  if ( !activity ) {
    return std::nullopt;
  }
  return activity->loopCharacteristics;
}
 
void CPSolutionObserver::unvisitEntry(const Vertex* vertex) {
//std::cerr << "unvisited " << vertex->reference() << std::endl;
//  _solution.setVariableValue( cp->position.at(vertex), (double)position );
  assert( cp->visit.contains(vertex) );
  _solution.setVariableValue( cp->visit.at(vertex), false);
  assert( cp->status.contains(vertex) );
  _solution.setVariableValue( cp->status.at(vertex)[BPMNOS::Model::ExtensionElements::Index::Timestamp].value, 0.0 );
 
  if ( vertex->node->represents<BPMN::MessageThrowEvent>() ) {
    for ( auto candidate : vertex->recipients ) {
      assert( candidate->exit<BPMN::MessageCatchEvent>() );
      assert( cp->messageFlow.contains({vertex,candidate}) );
      _solution.setVariableValue( cp->messageFlow.at({vertex,candidate}), (double)false );
    }
  }
 
  if (
    vertex->node->represents<BPMN::Task>() &&
    !(vertex->node->represents<BPMN::TypedStartEvent>() || vertex->node->represents<BPMN::ReceiveTask>())
  ) {
    // if visited, operators may modify data and globals upon entry
    // if unvisited, data and globals are not changed
    for ( size_t i = 0; i < vertex->dataOwners.size(); i++ ) {
      auto dataOwner = vertex->dataOwners[i];
      if ( flattenedGraph->modifiesData(vertex,dataOwner) ) {
        auto index = (size_t)_solution.evaluate( cp->dataIndex.at(vertex)[i] ).value();
 
        auto extensionElements = dataOwner->node->extensionElements->as<BPMNOS::Model::ExtensionElements>();
        assert( extensionElements );
        for ( auto& attribute : extensionElements->data ) {
          auto defined = _solution.evaluate( cp->data.at({dataOwner,attribute.get()}).defined[index] ).value();
          auto value = _solution.evaluate( cp->data.at({dataOwner,attribute.get()}).value[index] ).value();
          _solution.setVariableValue( cp->data.at({dataOwner,attribute.get()}).defined[index+1], defined );
          _solution.setVariableValue( cp->data.at({dataOwner,attribute.get()}).value[index+1], value );
        }
      }
    }
    if ( flattenedGraph->modifiesGlobals(vertex) ) {
      auto index = (size_t)_solution.evaluate( cp->globalIndex.at(vertex) ).value();
      for ( size_t attributeIndex = 0; attributeIndex < cp->globals.size(); attributeIndex++ ) {
        auto defined = _solution.evaluate( cp->globals.at(attributeIndex).defined[index] ).value();
        auto value = _solution.evaluate( cp->globals.at(attributeIndex).value[index] ).value();
        _solution.setVariableValue( cp->globals.at(attributeIndex).defined[index+1], defined );
        _solution.setVariableValue( cp->globals.at(attributeIndex).value[index+1], value );
      }
    }
  }
}
 
void CPSolutionObserver::unvisitExit(const Vertex* vertex) {
//std::cerr << "unvisited " << vertex->reference() << std::endl;
  assert( cp->visit.contains(vertex) );
//  _solution.setVariableValue( cp->position.at(vertex), (double)position );
  _solution.setVariableValue( cp->visit.at(vertex), false);
  assert( cp->status.contains(vertex) );
  _solution.setVariableValue( cp->status.at(vertex)[BPMNOS::Model::ExtensionElements::Index::Timestamp].value, 0.0 );
 
  if ( vertex->node->represents<BPMN::MessageCatchEvent>() ) {
    for ( auto candidate : vertex->senders ) {
      assert( candidate->entry<BPMN::MessageThrowEvent>() );
      assert( cp->messageFlow.contains({candidate,vertex}) );
      _solution.setVariableValue( cp->messageFlow.at({candidate,vertex}), (double)false );
    }
 
    if ( cp->locals.contains(vertex) ) {
      // only receive tasks and message start events have locals
      setLocalStatusValue( vertex, BPMNOS::Model::ExtensionElements::Index::Timestamp, 0.0 );
    }
 
    assert( cp->messageContent.contains(vertex) );
    for ( auto& [_, contentVariables] : cp->messageContent.at(vertex) ) {
      _solution.setVariableValue( contentVariables.defined, (double)false );
      _solution.setVariableValue( contentVariables.value, 0.0 );
    }
  }
 
  if ( vertex->node->represents<BPMNOS::Model::DecisionTask>() ) {
    // instant choices: timestamp is deduced from entry, only reset choice values and discretizers
    auto extensionElements = vertex->node->extensionElements->as<BPMNOS::Model::ExtensionElements>();
    for ( auto& choice : extensionElements->choices ) {
      // reset choice value
      setLocalStatusValue( vertex, choice->attribute->index, 0.0 );
      // reset discretizer if multipleOf constraint exists
      if ( choice->multipleOf && cp->discretizerMap.contains({vertex, choice->attribute}) ) {
        _solution.setVariableValue( cp->discretizerMap.at({vertex, choice->attribute}), 0.0 );
      }
    }
  }
 
  if ( vertex->node->represents<BPMN::TypedStartEvent>() || vertex->node->represents<BPMN::ReceiveTask>() ) {
    // if visited, operators may modify data and globals upon exit
    // if unvisited, data and globals are not changed
    for ( size_t i = 0; i < vertex->dataOwners.size(); i++ ) {
      auto dataOwner = vertex->dataOwners[i];
      if ( flattenedGraph->modifiesData(vertex,dataOwner) ) {
        auto index = (size_t)_solution.evaluate( cp->dataIndex.at(exit(vertex))[i] ).value();
 
        auto extensionElements = dataOwner->node->extensionElements->as<BPMNOS::Model::ExtensionElements>();
        assert( extensionElements );
        for ( auto& attribute : extensionElements->data ) {
          auto defined = _solution.evaluate( cp->data.at({dataOwner,attribute.get()}).defined[index-1] ).value();
          auto value = _solution.evaluate( cp->data.at({dataOwner,attribute.get()}).value[index-1] ).value();
          _solution.setVariableValue( cp->data.at({dataOwner,attribute.get()}).defined[index], defined );
          _solution.setVariableValue( cp->data.at({dataOwner,attribute.get()}).value[index], value );
        }
      }
    }
    if ( flattenedGraph->modifiesGlobals(vertex) ) {
      auto index = (size_t)_solution.evaluate( cp->globalIndex.at(exit(vertex)) ).value();
      for ( size_t attributeIndex = 0; attributeIndex < cp->globals.size(); attributeIndex++ ) {
        auto defined = _solution.evaluate( cp->globals.at(attributeIndex).defined[index-1] ).value();
        auto value = _solution.evaluate( cp->globals.at(attributeIndex).value[index-1] ).value();
        _solution.setVariableValue( cp->globals.at(attributeIndex).defined[index], defined );
        _solution.setVariableValue( cp->globals.at(attributeIndex).value[index], value );
      }
    }
  }
  
   if ( vertex->node->represents<BPMN::TypedStartEvent>() ) {
     // unvisit subsequent typed start events
     for ( auto successor : vertex->successors ) {
       if ( successor->node == vertex->node ) {
         setPosition( successor, ++lastPosition );
         unvisitEntry(successor);
         setPosition( exit(successor), ++lastPosition );
         unvisitExit(exit(successor));         
         finalizeUnvisitedSubsequentPositions(exit(successor));
         break;
       }
     }
   }
}
 
void CPSolutionObserver::synchronizeStatus(const BPMNOS::Values& status, const CPSolutionObserver::Vertex* vertex) {
  assert( cp->status.contains(vertex) );
  auto& statusVariables = cp->status.at(vertex);
  assert( status.size() == statusVariables.size() );
  for (size_t i = 0; i < statusVariables.size(); i++) {
    CPModel::AttributeEvaluation evaluation(
      _solution.evaluate( statusVariables[i].defined ),
      _solution.evaluate( statusVariables[i].value )
    );
    if ( status[i].has_value() ) {
      if ( !evaluation ) {
        // set solution value
        _solution.setVariableValue( statusVariables[i].defined, true );
        _solution.setVariableValue( statusVariables[i].value, (double)status[i].value() );
      }
      else if ( 
        !evaluation.defined()  ||
        evaluation.value() != status[i].value()
      ) {
 
std::cerr << "status[" << i << "].defined: " << (evaluation.defined() ? "true" : "false") << ", value: " << evaluation.value() << std::endl;
std::cerr << statusVariables[i].defined.stringify() << std::endl;
std::cerr << statusVariables[i].value.stringify() << std::endl;
//std::cerr << "Model: " << cp->stringify() << std::endl;
//std::cerr << "Solution: " <<  _solution.stringify() << std::endl;
        throw std::logic_error("CPSolutionObserver: inconsistent status '" + _solution.stringify(statusVariables[i].defined) + "' (observed as 'true') or '" + _solution.stringify(statusVariables[i].value) + "' (observed as '" + std::to_string((double)status[i].value_or(0)) + "')" );
      }
    }
    else {
      if ( !evaluation ) {
        // set solution value
        _solution.setVariableValue( statusVariables[i].defined, false );
        _solution.setVariableValue( statusVariables[i].value, 0.0 );
      }
      else if ( 
        evaluation.defined()  ||
        evaluation.value() != 0.0
      ) {
//std::cerr << "defined: " << (evaluation.defined() ? "true" : "false") << ", value: " << evaluation.value() << std::endl;
        throw std::logic_error("CPSolutionObserver: inconsistent status '" + _solution.stringify(statusVariables[i].defined) + "' (observed as 'false') or '" + _solution.stringify(statusVariables[i].value) + "' (observed as '0.0')" );
      }
    }
  }
}
 
void CPSolutionObserver::synchronizeData(const BPMNOS::SharedValues& data, const CPSolutionObserver::Vertex* vertex) {
  assert( cp->dataIndex.contains(vertex) );
  auto& dataIndices = cp->dataIndex.at(vertex);
  assert( dataIndices.size() == vertex->dataOwners.size() );
  // iterate over the data indices for each data owner
  for ( size_t i = 0; i < dataIndices.size(); i++ ) {
    auto indexEvaluation = _solution.evaluate( dataIndices[i] );
    if ( !indexEvaluation ) {
std::cerr << dataIndices[i].stringify() << std::endl;
      throw std::logic_error("CPSolutionObserver: Unable to determine data index for '" + vertex->reference() + "\n'" + indexEvaluation.error());
    }
    auto index = (size_t)indexEvaluation.value();
    auto ownerVertex = vertex->dataOwners[i];
    assert( ownerVertex->entry<BPMN::Scope>() );
//std::cerr << "set data[" << ownerVertex.shortReference() << ", "<< index << "] for " << vertex->reference() << std::endl;
    auto scope = ownerVertex->node;
    auto extensionElements = scope->extensionElements->as<BPMNOS::Model::ExtensionElements>();
    for ( auto& attribute : extensionElements->data ) {
      if ( attribute->index == BPMNOS::Model::ExtensionElements::Index::Instance ) {
        continue;
      }
      auto& indexedAttributeVariables = cp->data.at({ownerVertex,attribute.get()});
      // override solution value (positions and indices may have changed)
      if ( data[attribute->index].get().has_value() ) {
        _solution.setVariableValue( indexedAttributeVariables.defined[index], true );
        _solution.setVariableValue( indexedAttributeVariables.value[index], (double)data[attribute->index].get().value() );
      }
      else {
        _solution.setVariableValue( indexedAttributeVariables.defined[index], false );
        _solution.setVariableValue( indexedAttributeVariables.value[index], 0.0 );
      }
    }
  }
}
 
void CPSolutionObserver::synchronizeGlobals(const BPMNOS::Values& globals, const CPSolutionObserver::Vertex* vertex) {
  assert( cp->globalIndex.contains(vertex) );
  auto indexEvaluation = _solution.evaluate( cp->globalIndex.at(vertex) );
  if ( !indexEvaluation ) {
    throw std::logic_error("CPSolutionObserver: Unable to determine global index for '" + vertex->reference() + "\n'" + indexEvaluation.error());
  }
  auto index = (size_t)indexEvaluation.value();
  for ( size_t attributeIndex = 0; attributeIndex < globals.size(); attributeIndex++ ) {
    auto& indexedAttributeVariables = cp->globals[attributeIndex];
    // override solution value (positions and indices may have changed)
    if ( globals[attributeIndex].has_value() ) {
      _solution.setVariableValue( indexedAttributeVariables.defined[index], true );
      _solution.setVariableValue( indexedAttributeVariables.value[index], (double)globals[attributeIndex].value() );
    }
    else {
      _solution.setVariableValue( indexedAttributeVariables.defined[index], false );
      _solution.setVariableValue( indexedAttributeVariables.value[index], 0.0 );
    }
  }
}
 
/*
const CP::Solution& CPSolutionObserver::getSolution() const {
  return _solution;
}
*/
 
std::vector<size_t> CPSolutionObserver::getSequence() const {
  std::vector<size_t> sequence(flattenedGraph->vertices.size());
  for ( size_t i = 0; i < flattenedGraph->vertices.size(); i++ ) {
    sequence[ (size_t)_solution.getVariableValue( cp->position.at( flattenedGraph->vertices[i].get() ) ).value() -1 ] = i + 1;
  }
  
  return sequence;
}
 
size_t CPSolutionObserver::getPosition(const Vertex* vertex) const {
  assert( cp->position.contains( vertex ) );
  return (size_t)_solution.getVariableValue( cp->position.at( vertex ) ).value_or(0);
}
 
void CPSolutionObserver::initializePositions(const std::vector<double>& positions) {
  assert( positions.size() == flattenedGraph->vertices.size() );
  assert( cp->getModel().getSequences().size() == 1 );
  auto& sequenceVariable = cp->getModel().getSequences().front();
  _solution.setSequenceValues( sequenceVariable, positions );
}
 
void CPSolutionObserver::setPosition(const Vertex* vertex, size_t position) {
//std::cerr << "position(" << cp->indexMap.at(vertex) << ":" << vertex->reference() << ") = " << position << " / " << _solution.evaluate(cp->visit.at(vertex)).value_or(-1) << std::endl;
  assert( cp->position.contains( vertex ) );
  assert( _solution.getVariableValue( cp->position.at(vertex) ).has_value() );
  auto priorPosition = (size_t)_solution.getVariableValue( cp->position.at(vertex) ).value();
  assert( position <= priorPosition );
  if ( position < priorPosition ) {
    for ( auto& other : flattenedGraph->vertices ) {
      if ( other.get() == vertex ) {
        continue;
      }
      assert( _solution.getVariableValue( cp->position.at(other.get()) ).has_value() );
      auto otherPosition = (size_t)_solution.getVariableValue( cp->position.at(other.get()) ).value();
      if ( otherPosition >= position && otherPosition < priorPosition ) {
        // increment position of other vertex 
        _solution.setVariableValue( cp->position.at(other.get()), (double)++otherPosition );
      }
    }
  }
  // change vertex position
  _solution.setVariableValue( cp->position.at(vertex), (double)position );
//std::cerr << "changed position(" << vertex->reference() << ") from " <<  priorPosition << " to " << position << std::endl;
}
 
void CPSolutionObserver::finalizePosition(const Vertex* vertex) {
//std::cerr << "finalizePosition " << vertex->reference() << std::endl;
  if ( vertex->type == Vertex::Type::ENTRY && getLoopCharacteristics(vertex) ) {
    // finalize position of dummy for loop or multi-instance activity
    for ( auto [_,other] : vertex->inflows ) {
      if ( 
        other->node == vertex->node && 
        flattenedGraph->dummies.contains(other) &&
        _solution.getVariableValue( cp->position.at(other) ).value() > (double)lastPosition
      ) {
        // finalize position of dummy entry
        setPosition(other, ++lastPosition);
        break;
      }
    }
  }
 
  setPosition(vertex, ++lastPosition);
 
  if ( vertex->type == Vertex::Type::EXIT && getLoopCharacteristics(vertex) ) {
    // finalize position of dummy for loop or multi-instance activity
    for ( auto [_1,other] : vertex->outflows ) {
      if ( 
        other->node == vertex->node && 
        flattenedGraph->dummies.contains(other) 
      ) {
        bool isLast = true;
        for ( auto [_2,sibling] : other->inflows ) {
          if ( _solution.getVariableValue( cp->position.at(sibling) ).value() > (double)lastPosition ) {
            isLast = false;
            break;
          }
        }
        if ( isLast ) {
          // finalize position of dummy exit
          setPosition(other, ++lastPosition);
          break;
        }
      }
    }
  }
}
 
void CPSolutionObserver::finalizeUnvisitedSubsequentPositions(const Vertex* vertex) {
  for ( auto& [_1,other] : vertex->outflows ) {
    auto isVisited = _solution.evaluate( cp->visit.at(other) );
    if ( isVisited.has_value() && !isVisited.value() ) {
      // successor is not visited
      bool canBeFinalized = true;
      for ( auto& [_2, predecessor] : other->inflows ) {
        if ( predecessor != vertex && !markedFlows.contains({predecessor,other}) ) {
//std::cerr << "Unmarked flow from: " << predecessor->reference() << std::endl;
          canBeFinalized = false;
          break;
        }
      }
 
      markedFlows.insert({vertex,other});
//std::cerr << "Cannot finalize: " << other->reference() << std::endl;
      if ( !canBeFinalized ) {
        continue;
      }
      
      bool hasPendingPredecessors = false;
      for ( auto predecessor : other->predecessors ) {
        if ( _solution.getVariableValue( cp->position.at(predecessor) ).value() > (double)lastPosition ) {
//std::cerr << "hasPendingPredecessor: " << other->reference() << std::endl;
          hasPendingPredecessors = true;
          break;
        }
      }
      
      if ( hasPendingPredecessors ) {
        continue;
      }
 
      finalizePosition(other);
//std::cerr << "finalized: " << other->reference() << " position=" << lastPosition << " visited=false" << std::endl;
 
      if ( other->type == Vertex::Type::ENTRY ) {
        assert( !_solution.getVariableValue( cp->visit.at(other) ).has_value() );
        unvisitEntry(other);
      }
      else {
        assert( other->node->represents<BPMN::TypedStartEvent>() || _solution.getVariableValue( cp->visit.at(other) ).has_value() );
        unvisitExit(other);
      }
      finalizeUnvisitedSubsequentPositions(other);
    }
  }
}
 
bool CPSolutionObserver::isVisited(const Vertex* vertex) const {
  assert( cp->visit.contains( vertex ) );
  return _solution.evaluate( cp->visit.at( vertex ) ).value_or(false);
}
 
bool CPSolutionObserver::isUnvisited(const Vertex* vertex) const {
  assert( cp->visit.contains( vertex ) );
  return !_solution.evaluate( cp->visit.at( vertex ) ).value_or(true);
}
 
bool CPSolutionObserver::messageFlows( const Vertex* sender, const Vertex* recipient ) {
  assert( cp->messageFlow.contains( {sender,recipient} ) );
  return _solution.evaluate( cp->messageFlow.at( {sender,recipient} ) ).value_or(false);
}
 
 
std::optional< BPMNOS::number > CPSolutionObserver::getTimestamp( const Vertex* vertex ) const {
  assert( cp->status.contains(vertex) );
  assert( cp->status.at(vertex).size() > BPMNOS::Model::ExtensionElements::Index::Timestamp );
  auto timestamp = _solution.evaluate( cp->status.at(vertex)[BPMNOS::Model::ExtensionElements::Index::Timestamp].value );
  if ( timestamp ) {
    return (number)timestamp.value();
  }
  return std::nullopt;
}
 
void CPSolutionObserver::setTimestamp( const Vertex* vertex, BPMNOS::number timestamp ) {
  _solution.setVariableValue( cp->status.at(vertex)[BPMNOS::Model::ExtensionElements::Index::Timestamp].value, (double)timestamp );
}
 
std::optional< BPMNOS::number > CPSolutionObserver::getStatusValue( const Vertex* vertex, size_t attributeIndex ) const {
  if ( !_solution.evaluate( cp->status.at( vertex )[attributeIndex].defined ).has_value() ||  !_solution.evaluate( cp->status.at( vertex )[attributeIndex].defined ).value() ) {
    return std::nullopt;  
  }
  return _solution.evaluate( cp->status.at(vertex)[attributeIndex].value ).value(); 
}
 
void CPSolutionObserver::setTriggeredEvent( const Vertex* gateway, const Vertex* event ) {
//std::cerr << gateway->reference() << "/" << event->reference() << std::endl;
  assert( event->entry<BPMN::CatchEvent>() );
  assert( gateway->exit<BPMN::EventBasedGateway>() );
  for ( auto& [ _, target ] : gateway->outflows ) {
    _solution.setVariableValue( cp->tokenFlow.at({gateway,target}), ( target == event ) );
//std::cerr << "Token flow " << gateway.reference() << " to " << target.reference() << " = " << ( &target == entryVertex ) << std::endl;
  } 
}
 
 
void CPSolutionObserver::setLocalStatusValue( const Vertex* vertex, size_t attributeIndex, BPMNOS::number value ) {
  auto& initialStatus = std::get<0>(cp->locals.at(vertex)[0]);
  _solution.setVariableValue( initialStatus[attributeIndex].value, (double)value );
}
 
#endif // USE_CP