Recent changes to feature-requests

#16 Considerar formulas mas generales al compilar los safety de Update Controller

2015-07-08T09:25:32.335000Z

commit que soluciona esto: https://sourceforge.net/p/mtsa/code/1124/

#15 Permitir especificar con maquinas de estado los safety en un controllerSpec para Update Controllers

2015-07-07T09:17:10.672000Z

Creo que esto no es posible.

Lo que hacemos actualmente con las ltl_property que se declaran en safety = {A...}
es transformalas a las siguientes 2 formulas:

A W stopOldSpec
y
[]A">

Al ser ltl_property, en el codigo puedo hacer def.getLTLFormula() pero si son lts (ProcessSpec) no puedo hacer nada similar. Hay alguna solucion ?

#16 Considerar formulas mas generales al compilar los safety de Update Controller

2015-07-07T07:07:31.934000Z

Que otras formulas deberia considerar?

([]A || []B)

tambien entra en el scope?
otras mas complejas?

Considerar formulas mas generales al compilar los safety de Update Controller

2015-06-04T12:47:09.205000Z

Actualmente solo funciona correctamente para formulas de la forma
'' o simplemente formulas sin '[]'
Pero si la formula viene escrita de la siguiente forma:
F = ([]A && []B && ..) al transformar esta formula a 'F W stopOldSpec' no se generara controlador.

Permitir especificar con maquinas de estado los safety en un controllerSpec para Update Controllers

2015-06-04T12:42:25.425000Z

controllerSpec S = {
safety = {A, B, C}
}

Actualmente solo funciona si se usan ltl_property, pero A,B,C tambien podrian ser LTS.

Codigo en UpdatingControllersGoalsMaker#obtainFormula

Import Files

2015-03-06T17:40:21.834000Z

The tool must import files from others .lts

Add support for LTS bisimulation in FSP

2015-02-23T14:22:34.927000Z

Extend FSP to allow for bisimulation check. For example, bisimilar {C1,C2}.

Optimisation that avoid building strategies for loosing games

2015-02-19T16:58:36.031000Z

There is an optimisation to be made in every game solver. We could avoid building the strategy when the initial state of the game is not winning for the controller. This feature requires to add the set of initial states to the game structure, and extending the game interface to be able to answer if a game is winning or not. This applies to all game solvers -- e.g. GRGameSolver, ConcurrencyGRGameSolver.

#10 [Refactor] - Parametrize memory type

2015-01-05T13:46:33.875000Z

Commit revision # 968

Adapt applyUpdatingController method to Control Problem Class

2015-01-04T21:43:58.805000Z

Adapt the applyUpdatingController method in TransitionSystemDispatcher to Control Problem Class