spec/lib/collective_proof_attempt_spec.rb

	collective_proof_attempt_spec.rb revision dec646b1c869d05722892d5c4b22f45045aaaf53
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksarequire 'spec_helper'
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksadescribe CollectiveProofAttempt do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  setup_hets
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:prover) { Prover.first }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:user) { create :user }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:repository) { create :repository }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:ontology_fixture_file) { %w(prove/Simple_Implications casl) }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:ontology_filepath) { ontology_fixture_file.join('.') }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  before do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    stub_hets_for(ontology_filepath)
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    stub_hets_for(ontology_filepath, command: 'prove', method: :post)
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:parent_ontology_version) do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    version = version_for_file(repository,
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa                               ontology_file(*ontology_fixture_file))
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    version.parse
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    version
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:parent_ontology) { parent_ontology_version.ontology }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:ontology) { parent_ontology.children.find_by_name('Group') }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:ontology_version) { ontology.current_version }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:theorem) { ontology.theorems.find_by_name('rightunit') }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:theorem2) { ontology.theorems.find_by_name('zero_plus') }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:theorems) { [theorem, theorem2] }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:proof_attempt) { create :proof_attempt, theorem: theorem, prover: nil }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:proof_attempt2) { create :proof_attempt, theorem: theorem2, prover: nil }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:proof_attempts) { [proof_attempt, proof_attempt2] }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:status_open) { ProofStatus.find('OPN') }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  let(:status_proven) { ProofStatus.find('THM') }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa  context 'on theorem' do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    context 'before proving' do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      it "proof_attempt's proof_status is OPN" do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        expect(proof_attempt.reload.proof_status).to eq(status_open)
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      it "theorem's proof_status is OPN" do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        expect(theorem.reload.proof_status).to eq(status_open)
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa    context 'after proving' do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      let(:options_to_attempts) do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        {Hets::ProveOptions.new(prover: prover) => [proof_attempt]}
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      let(:cpa) { CollectiveProofAttempt.new(theorem, options_to_attempts) }
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      before do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        [cpa.send(:ontology_version), *theorems, *proof_attempts].each do |obj|
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa          allow(obj).to receive(:update_state!).and_call_original
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        cpa.run
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      it 'set state of theorem to processing' do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        expect(theorem).to have_received(:update_state!).with(:processing)
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      end
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      it 'set state of cpa.ontology_version to processing' do
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa        expect(cpa.send(:ontology_version)).
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa          to have_received(:update_state!).with(:processing)
dca00e3e210f3a3f814c63511f426128b1f3308cEugen Kuksa      end

      it 'cpa.ontology_version equals ontology_version' do
        expect(cpa.send(:ontology_version)).to eq(ontology_version)
      end

      it 'set state of proof_attempt to processing' do
        expect(proof_attempt).
          to have_received(:update_state!).with(:processing)
      end

      it "proof_attempt's proof_status is THM" do
        expect(proof_attempt.reload.proof_status).to eq(status_proven)
      end

      it "theorem's proof_status is THM" do
        expect(theorem.reload.proof_status).to eq(status_proven)
      end

      it "proof_attempt2's proof_status is OPN" do
        expect(proof_attempt2.reload.proof_status).to eq(status_open)
      end

      it "theorem2's proof_status is OPN" do
        expect(theorem2.reload.proof_status).to eq(status_open)
      end

      it 'state of proof_attempt is done in the end' do
        expect(proof_attempt.reload.state).to eq('done')
      end

      it 'state of theorem is done in the end' do
        expect(theorem.reload.state).to eq('done')
      end

      it "ontology_version's state is done in the end" do
        expect(ontology_version.reload.state).to eq('done')
      end
    end
  end

  context 'on ontology_version' do
    context 'before proving' do
      it "each proof_attempt's proof_status is OPN" do
        proof_attempts.each do |proof_attempt|
          expect(proof_attempt.reload.proof_status).to eq(status_open)
        end
      end

      it "each theorem's proof_status is OPN" do
        theorems.each do |theorem|
          expect(theorem.reload.proof_status).to eq(status_open)
        end
      end
    end

    context 'after proving' do
      let(:options_to_attempts) do
        {Hets::ProveOptions.new(prover: prover) => proof_attempts}
      end
      let(:cpa) do
        CollectiveProofAttempt.new(ontology_version, options_to_attempts)
      end
      before do
        [cpa.send(:ontology_version), *proof_attempts].each do |obj|
          allow(obj).to receive(:update_state!).and_call_original
        end
        cpa.run
      end

      it 'set state of cpa.ontology_version to processing' do
        expect(cpa.send(:ontology_version)).
          to have_received(:update_state!).with(:processing)
      end

      it 'cpa.ontology_version equals ontology_version' do
        expect(cpa.send(:ontology_version)).to eq(ontology_version)
      end

      it 'set state of each proof_attempt to processing' do
        proof_attempts.each do |proof_attempt|
          expect(proof_attempt).
            to have_received(:update_state!).with(:processing)
        end
      end

      it "each proof_attempt's proof_status is THM" do
        proof_attempts.each do |proof_attempt|
          expect(proof_attempt.reload.proof_status).to eq(status_proven)
        end
      end

      it "each theorem's proof_status is THM" do
        theorems.each do |theorem|
          expect(theorem.reload.proof_status).to eq(status_proven)
        end
      end

      it "each proof_attempt's is done in the end" do
        proof_attempts.each do |proof_attempt|
          expect(proof_attempt.reload.state).to eq('done')
        end
      end

      it "each theorem's state is done in the end" do
        theorems.each do |theorem|
          expect(theorem.reload.state).to eq('done')
        end
      end

      it "ontology_version's state is done in the end" do
        expect(ontology_version.reload.state).to eq('done')
      end
    end
  end
end