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
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 ?
Last edit: Victor Wjugow 2015-07-08
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:
Related
Feature Requests: #15