Spec should be higher level

[santolucito]

CYOA-TSL/spec engineering/CYOAxTSL.md

Line 13 in 2f84fd1

F [passage <- toCave()];

Why not

F inCave()

[ravenrothkopf]

i'm not sure I understand. wouldn't that be an assumption because inCave(passage) is an input from the environment which is already implied with this assumption? [passage <- toCave()] -> F inCave(passage); I have

F [passage <- toCave()]; 
F [passage <- toMarket()];

there to invoke the arbiter behavior, but lmk if you have other ideas on how to do this!

[santolucito]

It is an input from the environment but with the assumption it is not "fully controlled" by the environment. The environment needs to obey the assumption (or the assumption is false and we trivially win the game).

We want the system to not just update the passage with toMarket but keep doing that until we actually get to the market. So the spec really should say, force us to get the market, not just update the passage. Does that make sense?

[santolucito]

I say does it make sense because I'm not 100% sure it makes sense to me either

[ravenrothkopf]

yeah I think it does! like ideally the automaton should stay in the same state outputting toMarket() until atMarket() returns true. that seems to work okay with the spec I have.