# Copyright 2026 Paul Griffioen
#
# Permission is hereby granted, free of charge, to any person obtaining a copy
# of this software and associated documentation files (the "Software"), to deal
# in the Software without restriction, including without limitation the rights
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
# copies of the Software, and to permit persons to whom the Software is
# furnished to do so, subject to the following conditions:
#
# The above copyright notice and this permission notice shall be included in
# all copies or substantial portions of the Software.
#
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
# SOFTWARE.

import petri_net;
import random;
import fourier_motzkin;

include net_behavior;

run_examples();
example_random_run();
mini_max_test();

# This should give all pairs of moves for player 1 and player 2. The token clain
# and release part of the net alternates between two states. When both players 
# have made a move the net ends up in the same state. This means the moves form 
# a nullifier of the net.
fourier_motzkin(
    release_token_player_one + release_token_player_two -
    claim_token_player_one - claim_token_player_two);

# ------------------------------------------------------------------------------
#  Subtraction game tests
# ------------------------------------------------------------------------------

declare valid_game_moves :: List(Move);

define valid_game_moves = [
    Move@player_one_take_one,
    Move@player_two_take_two,
    Move@player_one_take_one,
    Move@player_two_take_three,
    Move@player_one_take_two,
    Move@player_two_take_one
];

define invalid_game_moves = [
    Move@player_one_take_one,
    Move@player_one_take_one
];

define run_examples() =
    begin
        print("\nRunning example 1");
        print("=================");
        run_subtraction_game(subtraction_game(10), valid_game_moves);

        print("\nRunning example 2");
        print("=================");
        run_subtraction_game(subtraction_game(10), invalid_game_moves);
    end;

# ------------------------------------------------------------------------------

define example_random_run() = 
    begin
        print("\nRunning random transitions");
        print("==========================");

        _ := run_petri_net_random(subtraction_game(10), 10);
    end;

# ------------------------------------------------------------------------------

define mini_max_test() =
    begin
        print("\nSubtraction game test");
        print("=====================\n");

        print("Pile   Winner");
        print("---------------");
        for i <- naturals(15) do
            printf("%4d   %s", i, run_subtraction_game_mini_max(i));
        end
    end;

define run_subtraction_game_mini_max(n) =
    let
        evaluation(marking, maximizing) =
            if maximizing then 1 else -1 end,

        (score, trace) = run_petri_net_mini_max(subtraction_game(n), true, evaluation)
    in
        if score > 0 then "player 1" else "player 2" end
    end;

# ------------------------------------------------------------------------------
# The subtraction game (simple Nim variant)
# ------------------------------------------------------------------------------

declare subtraction_game ::
    (1) -> PetriNet(1, GameState!unit, Move!);

define subtraction_game(n) =
    let 
        initial_marking =
            n '.*' delta(GameState@pile) + delta(GameState@player_one_to_play),

        pile_consume =
            take_from_pile_player_one + take_from_pile_player_two,

        token_produce =
            release_token_player_one + release_token_player_two,

        token_consume =
            claim_token_player_one + claim_token_player_two
    in
        make_petri_net(
            pile_consume + token_consume,
            token_produce,
            initial_marking * |GameState!unit|)
    end;

# ------------------------------------------------------------------------------

declare run_subtraction_game ::
    (PetriNet(1, GameState!unit, Move!), List(Move)) -> Void;

define run_subtraction_game(net, moves) =
    begin
        print("\nRunning subtraction game\n");

        trace := [ delta(m) | m <- moves ];

        (final_net, valid, count, _, _) := run_petri_net_trace_verbose(net, trace);

        player_one_wins := is_zero(delta(GameState@player_two_to_play) * petri_net_marking(final_net));

        if valid then
            printf("\nThe winner is %s", if player_one_wins then "player 1" else "player 2" end);
        else
            printf("\nMove %d was invalid: %s", count + 1, nth(count, moves));
        end

    end;

# ------------------------------------------------------------------------------
# Petri Net Structure
# ------------------------------------------------------------------------------

defindex GameState = {
    pile,
    player_one_to_play,
    player_two_to_play
};

defindex Move = {
    player_one_take_one,
    player_one_take_two,
    player_one_take_three,
    player_two_take_one,
    player_two_take_two,
    player_two_take_three    
};

# ------------------------------------------------------------------------------

defunit token "tkn";
defunit object "obj";

defunit GameState!unit = {
    pile: object,
    player_one_to_play: token,
    player_two_to_play: token
};

# ------------------------------------------------------------------------------
# Petri net parts
# ------------------------------------------------------------------------------

defmatrix take_from_pile_player_one :: GameState!unit per Move! = {
    pile, player_one_take_one -> 1,
    pile, player_one_take_two -> 2,
    pile, player_one_take_three -> 3
};

defmatrix take_from_pile_player_two :: GameState!unit per Move! = {
    pile, player_two_take_one -> 1,
    pile, player_two_take_two -> 2,
    pile, player_two_take_three -> 3
};

defmatrix claim_token_player_one :: GameState!unit per Move! = {
    player_one_to_play, player_one_take_one -> 1,
    player_one_to_play, player_one_take_two -> 1,
    player_one_to_play, player_one_take_three -> 1
};

defmatrix claim_token_player_two :: GameState!unit per Move! = {
    player_two_to_play, player_two_take_one -> 1,
    player_two_to_play, player_two_take_two -> 1,
    player_two_to_play, player_two_take_three -> 1
};

defmatrix release_token_player_one :: GameState!unit per Move! = {
    player_two_to_play, player_one_take_one -> 1,
    player_two_to_play, player_one_take_two -> 1,
    player_two_to_play, player_one_take_three -> 1
};

defmatrix release_token_player_two :: GameState!unit per Move! = {
    player_one_to_play, player_two_take_one -> 1,
    player_one_to_play, player_two_take_two -> 1,
    player_one_to_play, player_two_take_three -> 1
};