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

[Victor Wjugow]

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

[Victor Wjugow]

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
[](startNewSpec => []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 ?

[Nicolas D' Ippolito]

Vic, ya estas en BA ? nos juntamos la semana que viene? hay varias cosas
para charlar.

Abrazo!
N

2015-07-07 6:17 GMT-03:00 Victor Wjugow vwjugow@users.sf.net:

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"> http://sourceforge.net/../startNewSpec%20=%3E%20%5B%5DA

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

---

• [feature-requests:#15]
  http://sourceforge.net/p/mtsa/feature-requests/15 Permitir especificar
  con maquinas de estado los safety en un controllerSpec para Update
  Controllers*

Status: open
Group: Next Release (example)
Labels: ControllerUpdate NewSyntax Doesn'tCompile
Created: Thu Jun 04, 2015 12:42 PM UTC by Victor Wjugow
Last Updated: Thu Jun 04, 2015 12:42 PM UTC
Owner: Victor Wjugow

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

Sent from sourceforge.net because you indicated interest in
https://sourceforge.net/p/mtsa/feature-requests/15/

To unsubscribe from further messages, please visit
https://sourceforge.net/auth/subscriptions/