Restructure repo

[leoqiao18]

Clean up repo:

1. use package.yaml to replace tsl.cabal
2. reorganize project structure to be a more traditional app (executable), src (library) and test (tests) structure
3. remove tools and tool-utilities, and only have a single tsl command (implemented in app directory)
4. more obvious pipeline passes

[leoqiao18]

@santolucito Done. Can you take a look at this PR and see if the changes are ok with you? Made some drastic changes.

The new command now looks like this:

$ stack run -- tsl --help
tsl

Usage: tsl COMMAND

  TSL synthesis tool

Available options:
  -h,--help                Show this help text

Available commands:
  preprocess               TSL -> Core TSL
  theorize                 TSL -> theory-encoded Core TSL
  tlsf                     TSL -> LTL under-approximation in TLSF format
  hoa                      TSL -> synthesized controller in HOA format
  synthesize               TSL -> synthesized program in target language

[santolucito]

what about these: https://github.com/Barnard-PL-Labs/tsltools/#debugging-tsl-specifications. We still need these

[leoqiao18]

what about these: https://github.com/Barnard-PL-Labs/tsltools/#debugging-tsl-specifications. We still need these

I will add them in.

[leoqiao18]

@santolucito I added back the functionalities of tslminrealizable and tslcoregen. The last one for debugging is tslplay, which uses the CFM stuff. Does that mean we don't need it anymore?

[santolucito]

so tslplay should let us "play" against a counter strategy. So it is good functionality to have in theory, though I only got it to actually work once and it wasn't easy. maybe we leave it out for this PR and open an issue that we need to revisit it

…

On Fri, Nov 17, 2023 at 3:35 PM Leo Qiao ***@***.***> wrote: @santolucito <https://github.com/santolucito> I added back the functionalities of tslminrealizable and tslcoregen. The last one for debugging is tslplay, which uses the CFM stuff. Does that mean we don't need it anymore? — Reply to this email directly, view it on GitHub <#60 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAIJAPHFEVMG5XIXZ4FG6ZTYE7DCTAVCNFSM6AAAAAA7NOQYNGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQMJXGA3DQNJSGI> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[leoqiao18]

so tslplay should let us "play" against a counter strategy. So it is good functionality to have in theory, though I only got it to actually work once and it wasn't easy. maybe we leave it out for this PR and open an issue that we need to revisit it
…
On Fri, Nov 17, 2023 at 3:35 PM Leo Qiao @.> wrote: @santolucito https://github.com/santolucito I added back the functionalities of tslminrealizable and tslcoregen. The last one for debugging is tslplay, which uses the CFM stuff. Does that mean we don't need it anymore? — Reply to this email directly, view it on GitHub <#60 (comment)>, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIJAPHFEVMG5XIXZ4FG6ZTYE7DCTAVCNFSM6AAAAAA7NOQYNGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQMJXGA3DQNJSGI . You are receiving this because you were mentioned.Message ID: @.>

Ok, that sounds reasonable. I will update the README now, and after that can I merge this in?

[leoqiao18]

Issue that will document the development of the commands: #62

[santolucito]

lgtm!