diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml index 1c044fe73..4aaf1ae27 100644 --- a/.github/workflows/buildtest.yml +++ b/.github/workflows/buildtest.yml @@ -1,5 +1,5 @@ -name: Build Deploy -# Builds and and deploys image of Paynt with additional dependencies to Dockerhub +name: Build Test +# Builds and tests paynt and deploys images to Dockerhub on: push: @@ -19,27 +19,49 @@ env: NR_JOBS: "2" jobs: - deploy-learning: - name: Deploy on latest with learning dependencies (${{ matrix.buildType.name }}) + + deploy: + name: Deploy on latest (${{ matrix.buildType.name }}) runs-on: ubuntu-latest strategy: matrix: buildType: - - {name: "Release", baseImageName : "randriu/paynt", imageName : "marisgg/paynt-learner", dockerTag: "latest", setupArgs: ""} + - {name: "Release", imageName : "randriu/paynt", dockerTag: "latest", setupArgs: ""} fail-fast: false steps: - name: Git clone uses: actions/checkout@v4 - - name: Build paynt image with learner dependencies - run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . -f Dockerfile --build-arg paynt_base=${{ matrix.buildType.baseImageName }}:${{ matrix.buildType.dockerTag }} + - name: Build paynt image from Dockerfile + run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} - name: Login into docker - uses: docker/login-action@v3 - with: - username: ${{ secrets.DOCKERHUB_USERNAME }} - password: ${{ secrets.DOCKERHUB_TOKEN }} - # Only login if using master on this forked repo - if: github.repository_owner == 'marisgg' && github.ref == 'refs/heads/master' - - name: Deploy paynt image with learner dependencies - # Only deploy if using master on this forked repo - if: github.repository_owner == 'marisgg' && github.ref == 'refs/heads/master' + # Only login if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + run: echo '${{ secrets.STORMPY_CI_DOCKER_PASSWORD }}' | docker login -u randriu --password-stdin + - name: Deploy paynt image + # Only deploy if using master on original repo (and not for pull requests or forks) + if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' run: docker push ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} + + # deploy-learning: + # name: Deploy on latest with learning dependencies (${{ matrix.buildType.name }}) + # runs-on: ubuntu-latestx + # strategy: + # matrix: + # buildType: + # - {name: "Release", imageName : "randriu/paynt", dockerTag: "latest", setupArgs: ""} + # fail-fast: false + # steps: + # - name: Git clone + # uses: actions/checkout@v4 + # - name: Build paynt image from Dockerfile + # run: docker build -t ${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} . --build-arg setup_args=${{ matrix.buildType.setupArgs }} --build-arg setup_args_pycarl=${{ matrix.buildType.setupArgs }} --build-arg no_threads=${NR_JOBS} + # - name: Build paynt image with learner dependencies + # run: docker build -t ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} . -f paynt-learner.dockerfile --build-arg paynt_base=${{ matrix.buildType.imageName }}:${{ matrix.buildType.dockerTag }} + # - name: Login into docker + # # Only login if using master on original repo (and not for pull requests or forks) + # if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + # run: echo '${{ secrets.STORMPY_CI_DOCKER_PASSWORD }}' | docker login -u randriu --password-stdin + # - name: Deploy paynt image with learner dependencies + # # Only deploy if using master on original repo (and not for pull requests or forks) + # if: github.repository_owner == 'randriu' && github.ref == 'refs/heads/master' + # run: docker push ${{ matrix.buildType.imageName }}-learner:${{ matrix.buildType.dockerTag }} diff --git a/Dockerfile b/Dockerfile index 0125b77ff..8745bb729 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,21 +1,24 @@ -ARG paynt_base=randriu/paynt:ci +FROM movesrwth/stormpy:ci -# Pull paynt -FROM $paynt_base +# Additional arguments for compiling payntbind +ARG setup_args="" +# Number of threads to use for parallel compilation +ARG no_threads=2 -WORKDIR /opt/learning +WORKDIR /opt/ -# Install PyTorch and Jax with CUDA support. -RUN pip install torch==2.4.* "jax[cuda12]" +# install dependencies +RUN apt-get update -qq +RUN apt-get install -y graphviz +RUN pip install click z3-solver psutil graphviz -# Additional dependencies. -RUN pip install ipykernel joblib tensorboard==2.15.* einops==0.7.* gym==0.22.* pygame==2.5.* tqdm +# build paynt +WORKDIR /opt/paynt +COPY . . +WORKDIR /opt/paynt/payntbind +RUN python setup.py build_ext $setup_args -j $no_threads develop -RUN apt-get update && apt-get install -y curl +WORKDIR /opt/paynt -# install VS Code (code-server) -RUN curl -fsSL https://code-server.dev/install.sh | sh - -# install VS Code extensions -RUN code-server --install-extension ms-python.python \ - --install-extension ms-toolsai.jupyter +# (optional) install paynt +RUN pip install -e . diff --git a/paynt_pomdp_sketch.py b/paynt_pomdp_sketch.py deleted file mode 100644 index bf32e6dd6..000000000 --- a/paynt_pomdp_sketch.py +++ /dev/null @@ -1,98 +0,0 @@ -# using Paynt for POMDP sketches - -import paynt.cli -import paynt.parser.sketch -import paynt.quotient.pomdp_family -import paynt.quotient.fsc -import paynt.synthesizer.synthesizer_onebyone -import paynt.synthesizer.synthesizer_ar - -import payntbind - -import os -import random -import cProfile, pstats - -def load_sketch(project_path): - project_path = os.path.abspath(project_path) - sketch_path = os.path.join(project_path, "sketch.templ") - properties_path = os.path.join(project_path, "sketch.props") - pomdp_sketch = paynt.parser.sketch.Sketch.load_sketch(sketch_path, properties_path) - return pomdp_sketch - -def assignment_to_pomdp(pomdp_sketch, assignment): - pomdp = pomdp_sketch.build_pomdp(assignment).model - updated = payntbind.synthesis.restoreActionsInAbsorbingStates(pomdp) - if updated is not None: pomdp = updated - action_labels,_ = payntbind.synthesis.extractActionLabels(pomdp); - num_actions = len(action_labels) - pomdp,choice_to_true_action = payntbind.synthesis.enableAllActions(pomdp) - observation_action_to_true_action = [None]* pomdp.nr_observations - for state in range(pomdp.nr_states): - obs = pomdp.observations[state] - if observation_action_to_true_action[obs] is not None: - continue - observation_action_to_true_action[obs] = [None] * num_actions - choice_0 = pomdp.transition_matrix.get_row_group_start(state) - for action in range(num_actions): - choice = choice_0+action - true_action = choice_to_true_action[choice] - observation_action_to_true_action[obs][action] = true_action - return pomdp,observation_action_to_true_action - -def random_fsc(pomdp_sketch, num_nodes): - num_obs = pomdp_sketch.num_observations - fsc = paynt.quotient.fsc.FSC(num_nodes, num_obs) - # action function if of type NxZ -> Distr(Act) - for n in range(num_nodes): - for z in range(num_obs): - actions = pomdp_sketch.observation_to_actions[z] - fsc.action_function[n][z] = { action:1/len(actions) for action in actions } - # memory update function is of type NxZ -> Distr(N) and is posterior-aware - # note: this is currently inconsistent with definitions in paynt.quotient.fsc.FSC, but let's see how this works - for n in range(num_nodes): - for z in range(num_obs): - actions = pomdp_sketch.observation_to_actions[z] - fsc.update_function[n][z] = { n_new:1/num_nodes for n_new in range(num_nodes) } - return fsc - - -def main(): - profiling = True - if profiling: - profiler = cProfile.Profile() - profiler.enable() - - # random.seed(11) - - # enable PAYNT logging - paynt.cli.setup_logger() - - # load sketch - # project_path="models/pomdp/sketches/obstacles" - project_path="models/pomdp/sketches/avoid-discounted" - pomdp_sketch = load_sketch(project_path) - - # construct POMDP from the given hole assignment - hole_assignment = pomdp_sketch.family.pick_any() - pomdp,observation_action_to_true_action = assignment_to_pomdp(pomdp_sketch,hole_assignment) - - # construct an arbitrary 3-FSC - fsc = random_fsc(pomdp_sketch,3) - - # unfold this FSC into the quotient POMDP to obtain the quotient MDP (DTMC sketch) - # negate specification since we are interested in violating/worst assignments - dtmc_sketch = pomdp_sketch.build_dtmc_sketch(fsc, negate_specification=True) - - # solve - synthesizer = paynt.synthesizer.synthesizer_ar.SynthesizerAR(dtmc_sketch) - synthesizer.run() - - - if profiling: - profiler.disable() - stats = profiler.create_stats() - pstats.Stats(profiler).sort_stats('tottime').print_stats(10) - - -main() \ No newline at end of file