GitLab

MSTA allows parameterized assertions:

fluent FL[j:1..5] = <msg[j],ack>

assert Prop(Id=1) = ([]<>FL[Id])

But the syntax for livenes goals in synthesis fails when they are used.

See example below:

const M = 2 //Number of locations per room

const N = 3 //Number of rooms

range Rooms = 1..N 

range Locations = 1..M

set Controllables = {go[Rooms][0..M],sense}

set Alphabet = {arrived[Rooms][0..M],yes.person,no.person}

‌

Room(Id=1) = Elem[0],

Elem[i:Locations] = (when (i<M) go[Id][i+1] -> arrived[Id][i+1] -> Elem[i+1] |

    when (i>0) go[Id][i-1] -> arrived[Id][i-1] -> Elem[i-1]).

‌

MovementModel = (go[Rooms][Locations] -> GoModel),

GoModel = (arrived[Rooms][Locations] -> MovementModel).

‌

Adjacency = InRoom1, //Start in room 0

InRoom1 = (go[1][Locations] -> InRoom1 | go[2][Locations] -> InRoom2), //From Room1 we can go to Room1 or Room2

InRoom2 = (go[2][Locations] -> InRoom2 | go[3][Locations] -> InRoom3), //From Room2 we can go to Room2 or Room3

InRoom3 = (go[3][Locations] -> InRoom3 | go[1][Locations] -> InRoom1). //From Room3 we can go to Room3 or Room1 

PersonSensor = (sense -> Sensing),

Sensing = ({yes.person,no.person} -> PersonSensor).

ltl_property SenseAtEachLoc = [](arrived[Rooms][Locations] -> (!go[Rooms][Locations] W {yes.person,no.person}))

||Environment = (forall[id:Rooms] Room(id) || MovementModel || Adjacency || PersonSensor || SenseAtEachLoc).

fluent WentLocRoom[j:1..N][i:0..M] = <arrived[j][i],yes.person>

fluent FoundPerson = <yes.person,Alphabet\{yes.person}>

assert VisitedRoom1 = ((WentLocRoom[1][0] && WentLocRoom[1][1] && WentLocRoom[1][2]) || FoundPerson)

assert VisitedRoom2 = ((WentLocRoom[2][0] && WentLocRoom[2][1] && WentLocRoom[2][2]) || FoundPerson)

assert VisitedRoom(Id=1) = ((forall[l:Locations] WentLocRoom[Id][l]) || FoundPerson)

controllerSpec ControlSpec = {

safety = {}

        assumption = {}

        liveness = {VisitedRoom(1),VisitedRoom(2)}

        controllable = {Controllables}

}

controller ||Controller = Environment~{ControlSpec}.