search

Barnard-PL-Labs / CYOA-TSL

Choose your own TSL adventure!
0 stars 1 forks source link

Spec should be higher level #1

Open santolucito opened 11 months ago

santolucito commented 11 months ago

https://github.com/Barnard-PL-Labs/CYOA-TSL/blob/2f84fd1f70b8a834f2ceefde78bde5aa8187b5f7/spec%20engineering/CYOAxTSL.md?plain=1#L13

Why not

F inCave()

ravenrothkopf commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

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

ravenrothkopf commented 11 months ago

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.