Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Introducing a website that will enhance discoverability. #504

Open
Neelanchal17 opened this issue Nov 5, 2024 · 24 comments
Open

Introducing a website that will enhance discoverability. #504

Neelanchal17 opened this issue Nov 5, 2024 · 24 comments

Comments

@Neelanchal17
Copy link

As a web developer, I’d love to contribute to JavaPathfinder by creating a website to enhance its discoverability. Given my background, I believe a dedicated site could significantly improve the user experience with documentations. With permission from the maintainers, I can begin work on this project.
Thank You
@cyrille-artho
Copy link
Member

Thank you for offering to write documentation. Perhaps the best type of documentation could be a tutorial? That could be a separate repository (as having a separate repository also takes care of demonstrating how to run an application that is not part of jpf-core with JPF). The repository could start with a simple example, similar but slightly more advanced than examples in src/examples in jpf-core, and build these independently against a known location of an existing installation of JPF.

Do you have some experience using JPF?

@venkat1701
Copy link

Hi @cyrille-artho, I'm a java content writer at Baeldung. I'd love to take this issue and contribute to add more advanced examples of using JPF. I do have previous experience of using JPF a little, and I believe that I can generate better scenarios in examples where it must be used. Do let me know if you want me to contribute to this.
Linkedin
Thanks!

@cyrille-artho
Copy link
Member

Hi @venkat1701 ,
Thank you for your offer. Why not try a small example first? We can then see how to update JPF and its wiki based on that.
For a larger example, it could be useful to have a separate repository. This way, people can also learn how to set up JPF for their own project.

@venkat1701
Copy link

Yes. But I'll need a little help setting up jpf-core as the given setup instructions don't work for me.

Here's an overview of the way I tried installing it:

  1. Cloned the repo
  2. Used build.gradle to build the project
  3. Faced issues in the package classes/jdk.internal.misc with errors probably related to module system.

@cyrille-artho
Copy link
Member

cyrille-artho commented Dec 16, 2024 via email

@venkat1701
Copy link

Hi, on running that, it gives me this: openjdk version "11.0.8-internal" 2020-07-14 OpenJDK Runtime Environment (build 11.0.8-internal+0-adhoc..jdk11u) OpenJDK 64-Bit Server VM (build 11.0.8-internal+0-adhoc..jdk11u, mixed mode)

I did setup the project successfully now, and tried running the files in src/examples. But they don't seem to produce the expected output.

For instance, running the DiningPhil.java produces this output:

13:46:00: Executing ':DiningPhil.main()'...

> Task :compileAnnotationsJava UP-TO-DATE
> Task :processAnnotationsResources NO-SOURCE
> Task :annotationsClasses UP-TO-DATE
> Task :copyLibs UP-TO-DATE
> Task :compileJava UP-TO-DATE
> Task :processResources NO-SOURCE
> Task :classes UP-TO-DATE
> Task :generateBuildInfo
> Task :generateVersion
> Task :copyResources
> Task :compileExamplesJava UP-TO-DATE
> Task :processExamplesResources NO-SOURCE
> Task :examplesClasses UP-TO-DATE
> Task :DiningPhil.main()

BUILD SUCCESSFUL in 480ms
8 actionable tasks: 4 executed, 4 up-to-date
13:46:01: Execution finished ':DiningPhil.main()'.

@cyrille-artho
Copy link
Member

cyrille-artho commented Dec 17, 2024 via email

@venkat1701
Copy link

Hi, thanks for the onboarding help. I've successfully setup the repo now and can start contributing. Let us create another issue and start over there with the simple examples and scenarios if you are alright with it or should we continue in this issue?

@cyrille-artho
Copy link
Member

We can use your new repo's issue tracker for smaller steps, and later on close this issue when we think we have enough examples/documentation for an initial "release".

@venkat1701
Copy link

Alright, I'll update you soon with a google document of what examples I can work on for initial release.
Also, how will we integrate the initial release here on the jpf-core repository?

@cyrille-artho
Copy link
Member

cyrille-artho commented Dec 20, 2024 via email

@venkat1701
Copy link

venkat1701 commented Dec 22, 2024 •
edited
Loading

Hi @cyrille-artho , thanks for the time, I've compiled a list of 2 examples so far. Here's the link to the document
Also, I think it might be better to create a dedicated repository within the JavaPathfinder project for tutorials instead of linking them to the documentation or wiki. This way, users exploring jpf-core can directly access the tutorial repository. Alternatively, I can create a new repository on my end, which JavaPathfinder can fork, similar to jpf-symbc. This will add to future prospects of having contributions to that repository during the GSoC period as well.

@venkat1701
Copy link

Hey @cyrille-artho, just a ping to check if you're okay. Once a green flag, I can start working on the above examples right away.
Thanks!

@cyrille-artho
Copy link
Member

Hi,
Sorry for the slow response. Your messages overlapped with the holiday period.
The examples look interesting and relevant. If you could add a few lines first about what the examples are intended to do (what purpose the implementation serves, how the code is organized in terms of classes and threads, how it is used), that would help a lot to get all the necessary context.
Do you have the examples in a repository somewhere? I think it would help to have a repository that includes JPF as a dependency, similar to jpf-symbc, as that can then serve to show how JPF can be integrated in an existing project.

@venkat1701
Copy link

Warm wishes of the New Year!
No, I havent deployed the examples in any repository right now. And yes we can surely proceed that way. Initializing it in a way that can make jpf-core as a dependency of the repository.
I'll add more about the examples and the purpose of the implementations with some diagrams if required too.

@cyrille-artho
Copy link
Member

cyrille-artho commented Jan 8, 2025 via email

@venkat1701
Copy link

Surely, I'll go ahead with making those examples more documented and better. We can begin with different modules for each example to cover the tutorial. It sure will take a little time but will make sure its better understanding the use of jpf. Since having ten examples or more can't be a solution, I will add some more features into it so as to cover a vast range of concurrency errors.

@cyrille-artho
Copy link
Member

cyrille-artho commented Jan 9, 2025 via email

@venkat1701
Copy link

Alright, let's go with this ahead. I'll initialize a repository and also add detailed explanations for the two examples.

@venkat1701
Copy link

Hey, just to mention, I'm working on it. I might be late to finish the initialization due to my semester exams, but will work on this full time to cover up and I'm sorry for the delay

@cyrille-artho
Copy link
Member

Thank you, please take your time.

@venkat1701
Copy link

https://java-discord.notion.site/Examples-for-JPF-Repo-190cc94ba8f280548ab3f3c037c1f117

Hi @cyrille-artho, lmk what you think about these updated examples. Once confirmed, It'll take me 2 days to setup and complete these 2 examples, whilst covering the documentation on setting up and using the jpf-core.

@cyrille-artho
Copy link
Member

Thanks, this looks very good. Some suggestions:

  • Start the content with a one-line summary of your work (e.g., "This repository contains a collection of example concurrency problems that can be analyzed with JPF."), followed by a paragraph with more detail. In that paragraph, explain what JPF is/does in a sentence or two, what features your examples show, and who the target audience is. This way, the one-line summary and the following paragraph help the discoverability of your site, and also guide someone who comes across it to see immediately if this is what they searched for. You can refer to the JPF repository and wiki for details, so there is no need to write about great detail about JPF. (The reader only needs a rough idea and can go to the JPF wiki for more information if needed.)
  • The formatting of the output of lstree looks a bit off. Perhaps you can use code-style markup or a different way to make the lines line up.
  • Start with a one-paragraph summary of how JPF is used when trying your example (referring to the JPF wiki for details on how to configure JPF), followed with "Integration with JPF (Java Pathfinder)". That part looks like it is general and applies to all examples. I would put the output of lstree after that text.
  • Finish the main page with a list of all examples: their names and a one-sentence summary.
  • Put the details of each example on separate pages.
  • In the pages that explain the examples, a diagram can help to understand what the examples do.

@venkat1701
Copy link

Sure, I'll incorporate these changes in the repository

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@cyrille-artho @Neelanchal17 @venkat1701