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 https://github.com/Barnard-PL-Labs/tsltools/pull/60#issuecomment-1817068522, 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!