Skip to content

A framework for formalizing fCM-related Objectives as ASK-CTL formulas

Notifications You must be signed in to change notification settings

AnjoSs/objective-framework

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

29 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

objective-framework

During the execution of fragment-based Case Models (fCM), the Knowledge Worker (KW) needs assistance with making decisions. The Objective Frameworks offers support by providing the opportunity to define Objectives that should be met in the future of the execution. The fCM's state space can then be analyzed according to the Objective with a state space query. This query searches for execution states that satisfy the Objective. The path to such a state can serve as assistance for making decisions.

The Objective Framework allows the KW to formally define state space queries on a high-level abstraction. It provides an interface to compose Objectives according to Data Objects, their states and Tasks of the fCM. The Objective is then compiled into a state space query. More information can be found in the paper 'Late Goal Modelling for Fragment-Based Case Management'.

The Objective Framework relies on the formal representation of fCMs as Colored Petri nets (CPN). The compiled state space queries can be applied to the CPN representation of fCMs provided by the fcm2cpn compiler. In the future, the state space queries will be automatically executable with the fcm-Engine.

image

For now, the state space queries can be manually analyzed with CPN Tools.

Content of the Repository

This repository is a Vue.js application. It uses the material design framework Vuetify. The interface is provided in src/components

The compiler of the input to state space queries can be found in src/compiler/compiler.js.

An example can be found in the example-folder. It contains the fragments of an exemplary process (example/fragments.png) that describes the submission and reviewing of papers for a conference. The formalized CPN of this fCM can be found in example/conference.cpn

Project setup

The project can be used with the latest version of npm.

To install all dependencies, run:

npm install

To run the project, run:

npm run serve

The application should then be available at http://localhost:8080.

Usage

In the following, let us consider the following examplary fragments of an fCM (It is also provided in ´example/fragments.png´):

image

To use the Objective Framework, run the project.

It is now possible to insert Data Objects with their states, and Tasks.

image

To create a new Objective, click Create New.

image

An Objective regards one execution state and can consist of desired Data Object states and enabled Tasks. The semantics for Data Objects and desired states is that for a chosen state at least one Data Object with that state should exist. All options are connected with the logic AND.

For the desired input, the state space query is automatically compiled. It can be copied and used for the analysis in CPN Tools. The CPN-representation of the example can be found in example/conference.cpn. To use it, run the latest version of CPN-Tools, which can be downloaded from here.

The state space query is an ASK-CTL formula. More information can be found here.

image

To execute it, first, the models state space must be generated. To do so, select the generate state space option in the state space tool and click into the net. Due to the size of the state space, this might take several minutes.

image

Also, the strongly connected components graph has to be computed. Choose the option in the state space tool and click on the net.

image

Next, the ASK-CTL compiler must be loaded. Choose the ML compiler in the simulation tool and compile the expression use (ogpath^"ASKCTL/ASKCTLloader.sml") by clicking on it.

image

Now, any ASK-CTL formula can be executed by choosing the ML compiler and clicking on it. To execute the state space query, copy it into a separate text field in the net. In the exemplary CPN, the previously created state space query is already given.

To execute the query from the current state, choose the 'Sim to State Space' option of the state space tool. The current state node will be returned in the execution status in the bottom left corner. Insert it into the state space query in the line eval_node Objective <current state>; and execute it.

image

image

The query returns a boolean indicating whether or not an execution state can be reached that satisfies the objective. For all possible successor states, it can be investigated which can lead to a satisfying state and which can't. This information assists Knowledge Worker, what tasks to execute.

To investigate the state space and the successor states of the current state, the state space can be visualized by using the state space tool.

image

Note

Due to ongoing changes in the fcm2cpn compiler, the compiled state space queries might need manual adjustments regarding the naming of tasks and pages. The namings with whitespace should be changed to using underscores in the CPN. Also, tasks in the CPN might have trailing numbers like ..._0. In such cases, the query has to be adjusted.

About

A framework for formalizing fCM-related Objectives as ASK-CTL formulas

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published