search

nasa / PLEXIL5

PLEXIL5 is a Formal Verification Environment for PLEXIL
17 stars 9 forks source link

Installation and usage issues #4

Open kmdalal opened 2 years ago

kmdalal commented 2 years ago

Dear Team,

I've taken an interest in PLEXIL5 for potential use on two NASA projects: a collaboration with JPL in which we need V&V for PLEXIL; and OceanWATERS (https://github.com/nasa/ow_simulator), the project I lead that uses PLEXIL for lander autonomy. I would like to introduce V&V here as well.

I briefly played with PLEXIL5 many years ago. At present I'm having problems installing and running it.

  1. The download directory for Maude listed in your README.md no longer exists. I have used this link instead, and got the latest version 3.1 for MacOS. I'm not sure if this is the correct version to use, and I had to edit your build.xml file with their new executable name.
  2. I'm unable to load your cruise control example plan. I've attached a snapshot of the error message.

Could you please advise? Thanks! Mike

PS: Cesar, I tried emailing you at your NASA address and it bounced.

plexil5-error1

cesaramh commented 2 years ago

Hi Mike,

Thanks for the email. I’m not longer at NASA. I moved last year to Amazon Web Services. I’m forwarding this to Aaron, who is leading the FM team and to Marco, who was the last person to work on PLEXIL5.

Regards,

-- Cesar

On Jan 20, 2022, at 7:09 PM, Michael Dalal @.***> wrote:

 Dear Team,

I've taken an interest in PLEXIL5 for potential use on two NASA projects: a collaboration with JPL in which we need V&V for PLEXIL; and OceanWATERS (https://github.com/nasa/ow_simulator), the project I lead that uses PLEXIL for lander autonomy. I would like to introduce V&V here as well.

I briefly played with PLEXIL5 many years ago. At present I'm having problems installing and running it.

The download directory for Maude listed in your README.md no longer exists. I have used this link instead, and got the latest version 3.1 for MacOS. I'm not sure if this is the correct version to use, and I had to edit your build.xml file with their new executable name. I'm unable to load your cruise control example plan. I've attached a snapshot of the error message. Could you please advise? Thanks! Mike

PS: Cesar, I tried emailing you at your NASA address and it bounced.

— Reply to this email directly, view it on GitHub, or unsubscribe. Triage notifications on the go with GitHub Mobile for iOS or Android. You are receiving this because you are subscribed to this thread.

kmdalal commented 2 years ago

Hi Cesar,

Thanks for connecting me with Aaron and Marco -- we have been corresponding via email.

I was surprised and sorry to hear you'd left NASA, but I know AWS has a strong formal methods team (two of Ames' folks joined their automated reasoning group a few years ago). Hope it's going well!

Best, Mike (michael dot dalal at nasa dot gov)

ayushgupta9906 commented 1 year ago

Please assign me this issue. I can work on it.