text:
package cfvbaibai.cardfantasy.battlestat;

public class BattleStat {

}

redpajama_set_name: RedPajamaGithub


text:
package org.switchyard.rhq.plugin;

import org.rhq.modules.plugins.jbossas7.json.Address;

/**
 * SwitchYard Constants
 */
public class SwitchYardConstants {
    /**
     * The SwitchYard subsystem address.
     */
    public static final Address ADDRESS_SWITCHYARD = new Address("subsystem=switchyard");

    /**
     * The invocation outcome flag.
     */
    public static final String INVOCATION_OUTCOME = "outcome";
    /**
     * The invocation result.
     */
    public static final String INVOCATION_RESULT = "result";
    /**
     * The failure description value.
     */
    public static final String INVOCATION_FAILURE_DESCRIPTION = "failure-description";
    /**
     * The successful outcome value.
     */
    public static final String OUTCOME_SUCCESS = "success";

    /**
     * The get-version operation
     */
    public static final String DMR_GET_VERSION = "get-version";
    /**
     * The read-application operation
     */
    public static final String DMR_READ_APPLICATION = "read-application";
    /**
     * The read-service operation
     */
    public static final String DMR_READ_SERVICE = "read-service";
    /**
     * The read-reference operation
     */
    public static final String DMR_READ_REFERENCE = "read-reference";
    /**
     * The show-metrics operation
     */
    public static final String DMR_SHOW_METRICS = "show-metrics";
    /**
     * The reset-metrics operation
     */
    public static final String DMR_RESET_METRICS = "reset-metrics";
    /**
     * The start-gateway operation
     */
    public static final String DMR_START_GATEWAY = "start-gateway";
    /**
     * The stop-gateway operation
     */
    public static final String DMR_STOP_GATEWAY = "stop-gateway";
    /**
     * The update-throttling operation
     */
    public static final String DMR_UPDATE_THROTTLING = "update-throttling";

    /**
     * The name parameter
     */
    public static final String PARAM_NAME = "name";
    /**
     * The type parameter
     */
    public static final String PARAM_TYPE = "type";
    /**
     * The application-name parameter
     */
    public static final String PARAM_APPLICATION_NAME = "application-name";
    /**
     * The service-name parameter
     */
    public static final String PARAM_SERVICE_NAME = "service-name";
    /**
     * The reference-name parameter
     */
    public static final String PARAM_REFERENCE_NAME = "reference-name";
    /**
     * The throttling parameter
     */
    public static final String PARAM_THROTTLING = "throttling";

    /**
     * The reset operation
     */
    public static final String OPERATION_RESET = "reset";
    /**
     * The start operation
     */
    public static final String OPERATION_START = "start";
    /**
     * The stop operation
     */
    public static final String OPERATION_STOP = "stop";
    /**
     * The setThrottling operation
     */
    public static final Object OPERATION_SET_THROTTLING = "setThrottling";
    /**
     * The enabled parameter
     */
    public static final String OPERATION_PARAMETER_ENABLED = "enabled";
    /**
     * The maxRequests parameter
     */
    public static final String OPERATION_PARAMETER_MAX_REQUESTS = "maxRequests";

    /**
     * The SwitchYard component key.
     */
    public static final String KEY_SWITCH_YARD = "SwitchYardSubsystem";
    /**
     * The SwitchYard component description.
     */
    public static final String DESCRIPTION_SWITCH_YARD = "Container for SwitchYard Applications";
    /**
     * The SwitchYard component name.
     */
    public static final String NAME_SWITCH_YARD = "SwitchYard";

    /**
     * The success count metric
     */
    public static final String METRIC_SUCCESS_COUNT = "SuccessCount";
    /**
     * The fault count metric
     */
    public static final String METRIC_FAULT_COUNT = "FaultCount";
    /**
     * The total count metric
     */
    public static final String METRIC_TOTAL_COUNT = "TotalCount";
    /**
     * The total processing time metric
     */
    public static final String METRIC_TOTAL_PROCESSING_TIME = "TotalProcessingTime";
    /**
     * The average processing time metric
     */
    public static final String METRIC_AVERAGE_PROCESSING_TIME = "AverageProcessingTime";
    /**
     * The minimum processing time metric
     */
    public static final String METRIC_MIN_PROCESSING_TIME = "MinProcessingTime";
    /**
     * The maximum processing time metric
     */
    public static final String METRIC_MAX_PROCESSING_TIME = "MaxProcessingTime";
    /**
     * The throttling enabled metric
     */
    public static final String METRIC_THROTTLING_ENABLED = "throttlingEnabled";
    /**
     * The throttling time period metric
     */
    public static final String METRIC_TIME_PERIOD = "TimePeriod";
    /**
     * The throttling max requests metric
     */
    public static final String METRIC_MAX_REQUESTS = "MaxRequests";
    /**
     * The state metric
     */
    public static final String METRIC_STATE = "State";
}


text:
using System;
using System.Collections.Generic;
using System.Linq;
using System.Runtime.InteropServices;
using System.Text;

#if __UNIFIED__
using Foundation;
using UIKit;
#else
using MonoTouch.Foundation;
using MonoTouch.UIKit;
#endif

namespace BigTed
{
    /// <summary>
    /// Contains several extensions for NSObject and derived classes.
    /// </summary>
    public static class NSObjectExtensions
    {

        [DllImport("/usr/lib/libobjc.dylib")]
        private static extern IntPtr object_getClassName(IntPtr obj);

        /// <summary>
        /// Returns the Objective-C class name of the NSObject instance.
        /// </summary>
        /// <param name="obj"></param>
        /// <returns></returns>
        public static string GetClassName(this NSObject obj)
        {
            return Marshal.PtrToStringAuto(object_getClassName(obj.Handle));
        }

    }
}


text:
package cz.pichlik.goodsentiment.server.handler;

import static java.util.Arrays.asList;
import static org.hamcrest.CoreMatchers.containsString;
import static org.hamcrest.CoreMatchers.hasItem;
import static org.hamcrest.CoreMatchers.hasItems;
import static org.hamcrest.CoreMatchers.startsWith;
import static org.junit.Assert.assertThat;
import static org.mockito.Matchers.any;
import static org.mockito.Matchers.anyBoolean;
import static org.mockito.Matchers.anyInt;
import static org.mockito.Matchers.anyString;
import static org.mockito.Matchers.endsWith;
import static org.mockito.Matchers.eq;
import static org.mockito.Mockito.doAnswer;
import static org.mockito.Mockito.mock;
import static org.mockito.Mockito.verify;
import java.io.File;
import java.io.FileReader;
import java.time.LocalDate;
import java.util.ArrayList;
import java.util.List;
import java.util.function.Consumer;

import org.apache.commons.io.IOUtils;
import org.hamcrest.core.StringEndsWith;
import org.junit.Before;
import org.junit.Test;
import org.mockito.ArgumentCaptor;

import cz.pichlik.goodsentiment.server.repository.S3RepositoryBase;

@SuppressWarnings("unchecked")
public class EventAggregatorTest {

    private static final String AGGREGATED_BUCKET = "aggregatedDatabucket";
    private EventAggregator eventAggregator;
    private S3RepositoryBase s3Repo = mock(S3RepositoryBase.class);
    private EventDataReader eventDataReader = mock(EventDataReader.class);

    @Before
    public void setUp() throws Exception {
        this.eventAggregator = new EventAggregator(AGGREGATED_BUCKET, eventDataReader, s3Repo);
        this.eventAggregator.setSeed(0);
        doAnswer((i) -> {
            Object[] arguments = i.getArguments();
            Consumer<List<String>> callback = (Consumer<List<String>>) arguments[3];
            callback.accept(new ArrayList<>(asList("0","DevOps","49.2","16.6167","Brno","Male","6","1449770125")));
            return null;
        }).when(eventDataReader).read(anyInt(), anyInt(), anyInt(), any(Consumer.class));
     }

    @Test
    public void resultCSVHasHeader() throws Exception{
        File resultFile = aggregateSingle();
        try(FileReader fr = new FileReader(resultFile)) {
            List<String> result = IOUtils.readLines(fr);
            assertThat("Missing the CSV header", result, hasItem("id,sentimentCode,orgUnit,latitude,longitude,city,gender,yearsInCompany,timestamp"));
        }
    }

    @Test
    public void idIsPresent() throws Exception{
        File resultFile = aggregateSingle();
        try(FileReader fr = new FileReader(resultFile)) {
            List<String> result = IOUtils.readLines(fr);
            assertThat(result, hasItems(startsWith("0")));
        }
    }

    @Test
    public void timestampIsDate() throws Exception{
        File resultFile = aggregateSingle();
        try(FileReader fr = new FileReader(resultFile)) {
            List<String> result = IOUtils.readLines(fr);
            assertThat(result, hasItems(StringEndsWith.endsWith("2015-12-10T17:55:25")));
        }
    }

    @Test
    public void fileHasPublicRead() {
        aggregateSingle();
        verify(s3Repo).save(eq(AGGREGATED_BUCKET), anyString(), any(File.class), eq(true));
    }

    @Test
    public void filenamEndsWithCSV() {
        aggregateSingle();
        verify(s3Repo).save(eq(AGGREGATED_BUCKET), endsWith(".csv"), any(File.class), any(Boolean.class));
    }

    @Test
    public void resultHasData() throws Exception{
        File resultFile = aggregateSingle();
        try(FileReader fr = new FileReader(resultFile)) {
            List<String> result = IOUtils.readLines(fr);
            assertThat(result, hasItems(containsString("0,DevOps,49.2,16.6167,Brno,Male,6")));
        }
    }

    @Test
    public void aggregateMoreDays() throws Exception{
        LocalDate from = LocalDate.of(2015, 9, 1);
        LocalDate to = LocalDate.of(2015, 9, 2);
        eventAggregator.aggregateDay(from, to);
        verify(eventDataReader).read(eq(2015), eq(9), eq(1), any(Consumer.class));
        verify(eventDataReader).read(eq(2015), eq(9), eq(2), any(Consumer.class));
    }

    private File aggregateSingle() {
        ArgumentCaptor<File> resultFile = ArgumentCaptor.forClass(File.class);
        eventAggregator.aggregateDay(2015, 12, 14);
        verify(s3Repo).save(eq(AGGREGATED_BUCKET), anyString(), resultFile.capture(), anyBoolean());
        return resultFile.getValue();
    }

}


text:
"""
Support for HydroQuebec.

Get data from 'My Consumption Profile' page:
https://www.hydroquebec.com/portail/en/group/clientele/portrait-de-consommation

For more details about this platform, please refer to the documentation at
https://home-assistant.io/components/sensor.hydroquebec/
"""
import logging
from datetime import timedelta

import requests
import voluptuous as vol

from homeassistant.components.sensor import PLATFORM_SCHEMA
from homeassistant.const import (
    CONF_USERNAME, CONF_PASSWORD,
    CONF_NAME, CONF_MONITORED_VARIABLES, TEMP_CELSIUS)
from homeassistant.helpers.entity import Entity
from homeassistant.util import Throttle
import homeassistant.helpers.config_validation as cv

REQUIREMENTS = ['pyhydroquebec==1.1.0']

_LOGGER = logging.getLogger(__name__)

KILOWATT_HOUR = 'kWh'  # type: str
PRICE = 'CAD'  # type: str
DAYS = 'days'  # type: str
CONF_CONTRACT = 'contract'  # type: str

DEFAULT_NAME = 'HydroQuebec'

REQUESTS_TIMEOUT = 15
MIN_TIME_BETWEEN_UPDATES = timedelta(hours=1)

SENSOR_TYPES = {
    'period_total_bill':
    ['Current period bill', PRICE, 'mdi:square-inc-cash'],
    'period_length':
    ['Current period length', DAYS, 'mdi:calendar-today'],
    'period_total_days':
    ['Total number of days in this period', DAYS, 'mdi:calendar-today'],
    'period_mean_daily_bill':
    ['Period daily average bill', PRICE, 'mdi:square-inc-cash'],
    'period_mean_daily_consumption':
    ['Period daily average consumption', KILOWATT_HOUR, 'mdi:flash'],
    'period_total_consumption':
    ['Total Consumption', KILOWATT_HOUR, 'mdi:flash'],
    'period_lower_price_consumption':
    ['Period Lower price consumption', KILOWATT_HOUR, 'mdi:flash'],
    'period_higher_price_consumption':
    ['Period Higher price consumption', KILOWATT_HOUR, 'mdi:flash'],
    'yesterday_total_consumption':
    ['Yesterday total consumption', KILOWATT_HOUR, 'mdi:flash'],
    'yesterday_lower_price_consumption':
    ['Yesterday lower price consumption', KILOWATT_HOUR, 'mdi:flash'],
    'yesterday_higher_price_consumption':
    ['Yesterday higher price consumption', KILOWATT_HOUR, 'mdi:flash'],
    'yesterday_average_temperature':
    ['Yesterday average temperature', TEMP_CELSIUS, 'mdi:thermometer'],
    'period_average_temperature':
    ['Period average temperature', TEMP_CELSIUS, 'mdi:thermometer'],
}

PLATFORM_SCHEMA = PLATFORM_SCHEMA.extend({
    vol.Required(CONF_MONITORED_VARIABLES):
        vol.All(cv.ensure_list, [vol.In(SENSOR_TYPES)]),
    vol.Required(CONF_USERNAME): cv.string,
    vol.Required(CONF_PASSWORD): cv.string,
    vol.Required(CONF_CONTRACT): cv.string,
    vol.Optional(CONF_NAME, default=DEFAULT_NAME): cv.string,
})

HOST = 'https://www.hydroquebec.com'
HOME_URL = '{}/portail/web/clientele/authentification'.format(HOST)
PROFILE_URL = ('{}/portail/fr/group/clientele/'
               'portrait-de-consommation'.format(HOST))
MONTHLY_MAP = (('period_total_bill', 'montantFacturePeriode'),
               ('period_length', 'nbJourLecturePeriode'),
               ('period_total_days', 'nbJourPrevuPeriode'),
               ('period_mean_daily_bill', 'moyenneDollarsJourPeriode'),
               ('period_mean_daily_consumption', 'moyenneKwhJourPeriode'),
               ('period_total_consumption', 'consoTotalPeriode'),
               ('period_lower_price_consumption', 'consoRegPeriode'),
               ('period_higher_price_consumption', 'consoHautPeriode'))
DAILY_MAP = (('yesterday_total_consumption', 'consoTotalQuot'),
             ('yesterday_lower_price_consumption', 'consoRegQuot'),
             ('yesterday_higher_price_consumption', 'consoHautQuot'))

def setup_platform(hass, config, add_devices, discovery_info=None):
    """Set up the HydroQuebec sensor."""
    # Create a data fetcher to support all of the configured sensors. Then make
    # the first call to init the data.

    username = config.get(CONF_USERNAME)
    password = config.get(CONF_PASSWORD)
    contract = config.get(CONF_CONTRACT)

    try:
        hydroquebec_data = HydroquebecData(username, password, contract)
        _LOGGER.info("Contract list: %s",
                     ", ".join(hydroquebec_data.get_contract_list()))
    except requests.exceptions.HTTPError as error:
        _LOGGER.error("Failt login: %s", error)
        return False

    name = config.get(CONF_NAME)

    sensors = []
    for variable in config[CONF_MONITORED_VARIABLES]:
        sensors.append(HydroQuebecSensor(hydroquebec_data, variable, name))

    add_devices(sensors, True)

class HydroQuebecSensor(Entity):
    """Implementation of a HydroQuebec sensor."""

    def __init__(self, hydroquebec_data, sensor_type, name):
        """Initialize the sensor."""
        self.client_name = name
        self.type = sensor_type
        self.entity_id = "sensor.{}_{}".format(name, sensor_type)
        self._name = SENSOR_TYPES[sensor_type][0]
        self._unit_of_measurement = SENSOR_TYPES[sensor_type][1]
        self._icon = SENSOR_TYPES[sensor_type][2]
        self.hydroquebec_data = hydroquebec_data
        self._state = None

    @property
    def name(self):
        """Return the name of the sensor."""
        return '{} {}'.format(self.client_name, self._name)

    @property
    def state(self):
        """Return the state of the sensor."""
        return self._state

    @property
    def unit_of_measurement(self):
        """Return the unit of measurement of this entity, if any."""
        return self._unit_of_measurement

    @property
    def icon(self):
        """Icon to use in the frontend, if any."""
        return self._icon

    def update(self):
        """Get the latest data from Hydroquebec and update the state."""
        self.hydroquebec_data.update()
        if self.type in self.hydroquebec_data.data:
            self._state = round(self.hydroquebec_data.data[self.type], 2)

class HydroquebecData(object):
    """Get data from HydroQuebec."""

    def __init__(self, username, password, contract=None):
        """Initialize the data object."""
        from pyhydroquebec import HydroQuebecClient
        self.client = HydroQuebecClient(
            username, password, REQUESTS_TIMEOUT)
        self._contract = contract
        self.data = {}

    def get_contract_list(self):
        """Return the contract list."""
        # Fetch data
        self._fetch_data()
        return self.client.get_contracts()

    def _fetch_data(self):
        """Fetch latest data from HydroQuebec."""
        from pyhydroquebec.client import PyHydroQuebecError
        try:
            self.client.fetch_data()
        except PyHydroQuebecError as exp:
            _LOGGER.error("Error on receive last Hydroquebec data: %s", exp)
            return

    @Throttle(MIN_TIME_BETWEEN_UPDATES)
    def update(self):
        """Return the latest collected data from HydroQuebec."""
        self._fetch_data()
        self.data = self.client.get_data(self._contract)[self._contract]


text:
<!DOCTYPE html>

    <link rel="stylesheet" href="/style/style.css">
    <link rel="stylesheet" href="/style/font-awesome.css">
    <link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/4.0.0-alpha.6/css/bootstrap.min.css"
    integrity="sha384-rwoIResjU2yc3z8GV/NPeZWAv56rSmLldC3R/AZzGRnGxQQKnKkoFVhFQhNUwEyJ" crossorigin="anonymous">


text:
import React, { Component } from 'react';
import {
  StyleSheet,
  Text,
  View,
  Navigator,
  ScrollView,
  ListView,
  RefreshControl,
} from 'react-native'
import NavigationBar from 'react-native-navbar';
var REQUEST_URL = 'https://calm-garden-29993.herokuapp.com/index/groupmembers/?';

class MemberMgmt extends Component {

    constructor(props, context) {
        super(props, context);
        this.state = {
            loggedIn: true,
            dataSource: new ListView.DataSource({
              rowHasChanged: (row1, row2) => row1 !== row2,
            }),
            loaded: false,
        };
        this.fetchData();
        this.bindMethods();
    }

    bindMethods() {
        if (! this.bindableMethods) {
            return;
        }

        for (var methodName in this.bindableMethods) {
            this[methodName] = this.bindableMethods[methodName].bind(this);
        }
    }

    componentDidMount () {
      this.fetchData();
    }

    backOnePage () {
      this.props.navigator.pop();
    }

    toQueryString(obj) {
      return obj ? Object.keys(obj).sort().map(function (key) {
          var val = obj[key];

          if (Array.isArray(val)) {
              return val.sort().map(function (val2) {
                  return encodeURIComponent(key) + '=' + encodeURIComponent(val2);
              }).join('&');
          }

          return encodeURIComponent(key) + '=' + encodeURIComponent(val);
      }).join('&') : '';
    }

    fetchData() {
    fetch(REQUEST_URL + this.toQueryString({"group": this.props.group_info.pk}))
      .then((response) => response.json())
      .then((responseData) => {
        console.log(JSON.parse(responseData.members));
        this.setState({
          dataSource: this.state.dataSource.cloneWithRows(JSON.parse(responseData.members)),
          loaded: true,
        });
      })
      .done();
    }

    render () {
        return (
        <Navigator
            renderScene={this.renderScene.bind(this)}
            navigator = {this.props.navigator}
           />
        );
      }

  renderScene (route, navigator) {
    const backButton = {
            title: "Back",
            handler: () => this.backOnePage(),
          };
    if (!this.state.loaded) {
          return (<View>
              <Text>Loading!</Text>
            </View>);
        }
        else if (this.state.loggedIn) {
          return (
            <View>
            <NavigationBar
                      title={{ title: "Members", tintColor: 'black', }}
                      style={{ backgroundColor: "white", }}
                      leftButton={backButton}
                      statusBar={{ tintColor: "white", }}
                    />
            <ListView

                dataSource = {this.state.dataSource}
                renderRow = {this.renderRegularMembers}
                style = {styles.listView}
                refreshControl={
                  <RefreshControl
                    refreshing={this.state.refreshing}
                    onRefresh={this._onRefresh.bind(this)}
                  />
                }
            />
            </View>
          );
        } else {
            this.props.navigator.push({id: "LoginPage", name:"Index"})
        }

  }

}

Object.assign(MemberMgmt.prototype, {
    bindableMethods : {
        renderRegularMembers (member) {
          return (
          <View style={styles.row}>
              <Text onPress={() => this.memberPressed(member)} style={styles.title}>{member.fields.first_name + " " + member.fields.last_name}</Text>
            </View>
          );
        },
        memberPressed(member) {
            this.props.navigator.push({id:"MemberEdit", name: "MemberEdit", passProps: {"member_info": member, "group_info": this.props.group_info}});
        },
    }
});

var styles = StyleSheet.create({
  container: {
    flex: 1,
    flexDirection: 'row',
    justifyContent: 'center',
    alignItems: 'center',
    backgroundColor: '#ff7f50',
  },
  rightContainer: {
    flex: 1,
  },
  title: {
    fontSize: 20,
    marginBottom: 8,
    textAlign: 'center',
  },
  row: {
    flexDirection: 'row',
    justifyContent: 'center',
    padding: 10,
    backgroundColor: '#F6F6F6',
  },
  year: {
    textAlign: 'center',
  },
  thumbnail: {
    width: 53,
    height: 81,
  },
  listView: {
    paddingTop: 0,
    paddingBottom: 550,
  },
  headTitle: {
    color: 'black',
    fontSize:  30 ,
    fontWeight: 'normal',
    fontFamily: 'Helvetica Neue',
    alignSelf: "center",
  },
});

module.exports = MemberMgmt;


text:
//
// Copyright (C) 2006 Andras Babos and Andras Varga
//
// This program is free software; you can redistribute it and/or
// modify it under the terms of the GNU Lesser General Public License
// as published by the Free Software Foundation; either version 2
// of the License, or (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Lesser General Public License for more details.
//
// You should have received a copy of the GNU Lesser General Public License
// along with this program; if not, see <http://www.gnu.org/licenses/>.
//

#include "inet/routing/ospfv2/messagehandler/MessageHandler.h"

#include "inet/networklayer/ipv4/ICMPMessage.h"
#include "inet/routing/ospfv2/router/OSPFRouter.h"

namespace inet {

namespace ospf {

MessageHandler::MessageHandler(Router *containingRouter, cSimpleModule *containingModule) :
    IMessageHandler(containingRouter),
    ospfModule(containingModule),
    helloHandler(containingRouter),
    ddHandler(containingRouter),
    lsRequestHandler(containingRouter),
    lsUpdateHandler(containingRouter),
    lsAckHandler(containingRouter)
{
}

void MessageHandler::messageReceived(cMessage *message)
{
    if (message->isSelfMessage()) {
        handleTimer(message);
    }
    else if (dynamic_cast<ICMPMessage *>(message)) {
        EV_ERROR << "ICMP error received -- discarding\n";
        delete message;
    }
    else {
        OSPFPacket *packet = check_and_cast<OSPFPacket *>(message);
        EV_INFO << "Received packet: (" << packet->getClassName() << ")" << packet->getName() << "\n";
        if (packet->getRouterID() == IPv4Address(router->getRouterID())) {
            EV_INFO << "This packet is from ourselves, discarding.\n";
            delete message;
        }
        else {
            processPacket(packet);
        }
    }
}

void MessageHandler::handleTimer(cMessage *timer)
{
    switch (timer->getKind()) {
        case INTERFACE_HELLO_TIMER: {
            Interface *intf;
            if (!(intf = reinterpret_cast<Interface *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid InterfaceHelloTimer.\n";
                delete timer;
            }
            else {
                printEvent("Hello Timer expired", intf);
                intf->processEvent(Interface::HELLO_TIMER);
            }
        }
        break;

        case INTERFACE_WAIT_TIMER: {
            Interface *intf;
            if (!(intf = reinterpret_cast<Interface *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid InterfaceWaitTimer.\n";
                delete timer;
            }
            else {
                printEvent("Wait Timer expired", intf);
                intf->processEvent(Interface::WAIT_TIMER);
            }
        }
        break;

        case INTERFACE_ACKNOWLEDGEMENT_TIMER: {
            Interface *intf;
            if (!(intf = reinterpret_cast<Interface *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid InterfaceAcknowledgementTimer.\n";
                delete timer;
            }
            else {
                printEvent("Acknowledgement Timer expired", intf);
                intf->processEvent(Interface::ACKNOWLEDGEMENT_TIMER);
            }
        }
        break;

        case NEIGHBOR_INACTIVITY_TIMER: {
            Neighbor *neighbor;
            if (!(neighbor = reinterpret_cast<Neighbor *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid NeighborInactivityTimer.\n";
                delete timer;
            }
            else {
                printEvent("Inactivity Timer expired", neighbor->getInterface(), neighbor);
                neighbor->processEvent(Neighbor::INACTIVITY_TIMER);
            }
        }
        break;

        case NEIGHBOR_POLL_TIMER: {
            Neighbor *neighbor;
            if (!(neighbor = reinterpret_cast<Neighbor *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid NeighborInactivityTimer.\n";
                delete timer;
            }
            else {
                printEvent("Poll Timer expired", neighbor->getInterface(), neighbor);
                neighbor->processEvent(Neighbor::POLL_TIMER);
            }
        }
        break;

        case NEIGHBOR_DD_RETRANSMISSION_TIMER: {
            Neighbor *neighbor;
            if (!(neighbor = reinterpret_cast<Neighbor *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid NeighborDDRetransmissionTimer.\n";
                delete timer;
            }
            else {
                printEvent("Database Description Retransmission Timer expired", neighbor->getInterface(), neighbor);
                neighbor->processEvent(Neighbor::DD_RETRANSMISSION_TIMER);
            }
        }
        break;

        case NEIGHBOR_UPDATE_RETRANSMISSION_TIMER: {
            Neighbor *neighbor;
            if (!(neighbor = reinterpret_cast<Neighbor *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid NeighborUpdateRetransmissionTimer.\n";
                delete timer;
            }
            else {
                printEvent("Update Retransmission Timer expired", neighbor->getInterface(), neighbor);
                neighbor->processEvent(Neighbor::UPDATE_RETRANSMISSION_TIMER);
            }
        }
        break;

        case NEIGHBOR_REQUEST_RETRANSMISSION_TIMER: {
            Neighbor *neighbor;
            if (!(neighbor = reinterpret_cast<Neighbor *>(timer->getContextPointer()))) {
                // should not reach this point
                EV_INFO << "Discarding invalid NeighborRequestRetransmissionTimer.\n";
                delete timer;
            }
            else {
                printEvent("Request Retransmission Timer expired", neighbor->getInterface(), neighbor);
                neighbor->processEvent(Neighbor::REQUEST_RETRANSMISSION_TIMER);
            }
        }
        break;

        case DATABASE_AGE_TIMER: {
            printEvent("Ageing the database");
            router->ageDatabase();
        }
        break;

        default:
            break;
    }
}

void MessageHandler::processPacket(OSPFPacket *packet, Interface *unused1, Neighbor *unused2)
{
    // see RFC 2328 8.2

    // packet version must be OSPF version 2
    if (packet->getVersion() == 2) {
        IPv4ControlInfo *controlInfo = check_and_cast<IPv4ControlInfo *>(packet->getControlInfo());
        int interfaceId = controlInfo->getInterfaceId();
        AreaID areaID = packet->getAreaID();
        Area *area = router->getAreaByID(areaID);

        if (area != nullptr) {
            // packet Area ID must either match the Area ID of the receiving interface or...
            Interface *intf = area->getInterface(interfaceId);

            if (intf == nullptr) {
                // it must be the backbone area and...
                if (areaID == BACKBONE_AREAID) {
                    if (router->getAreaCount() > 1) {
                        // it must be a virtual link and the source router's router ID must be the endpoint of this virtual link and...
                        intf = area->findVirtualLink(packet->getRouterID());

                        if (intf != nullptr) {
                            Area *virtualLinkTransitArea = router->getAreaByID(intf->getTransitAreaID());

                            if (virtualLinkTransitArea != nullptr) {
                                // the receiving interface must attach to the virtual link's configured transit area
                                Interface *virtualLinkInterface = virtualLinkTransitArea->getInterface(interfaceId);

                                if (virtualLinkInterface == nullptr) {
                                    intf = nullptr;
                                }
                            }
                            else {
                                intf = nullptr;
                            }
                        }
                    }
                }
            }
            if (intf != nullptr) {
                IPv4Address destinationAddress = controlInfo->getDestAddr();
                IPv4Address allDRouters = IPv4Address::ALL_OSPF_DESIGNATED_ROUTERS_MCAST;
                Interface::InterfaceStateType interfaceState = intf->getState();

                // if destination address is ALL_D_ROUTERS the receiving interface must be in DesignatedRouter or Backup state
                if (
                    ((destinationAddress == allDRouters) &&
                     (
                         (interfaceState == Interface::DESIGNATED_ROUTER_STATE) ||
                         (interfaceState == Interface::BACKUP_STATE)
                     )
                    ) ||
                    (destinationAddress != allDRouters)
                    )
                {
                    // packet authentication
                    if (authenticatePacket(packet)) {
                        OSPFPacketType packetType = static_cast<OSPFPacketType>(packet->getType());
                        Neighbor *neighbor = nullptr;

                        // all packets except HelloPackets are sent only along adjacencies, so a Neighbor must exist
                        if (packetType != HELLO_PACKET) {
                            switch (intf->getType()) {
                                case Interface::BROADCAST:
                                case Interface::NBMA:
                                case Interface::POINTTOMULTIPOINT:
                                    neighbor = intf->getNeighborByAddress(controlInfo->getSrcAddr());
                                    break;

                                case Interface::POINTTOPOINT:
                                case Interface::VIRTUAL:
                                    neighbor = intf->getNeighborByID(packet->getRouterID());
                                    break;

                                default:
                                    break;
                            }
                        }
                        switch (packetType) {
                            case HELLO_PACKET:
                                helloHandler.processPacket(packet, intf);
                                break;

                            case DATABASE_DESCRIPTION_PACKET:
                                if (neighbor != nullptr) {
                                    ddHandler.processPacket(packet, intf, neighbor);
                                }
                                break;

                            case LINKSTATE_REQUEST_PACKET:
                                if (neighbor != nullptr) {
                                    lsRequestHandler.processPacket(packet, intf, neighbor);
                                }
                                break;

                            case LINKSTATE_UPDATE_PACKET:
                                if (neighbor != nullptr) {
                                    lsUpdateHandler.processPacket(packet, intf, neighbor);
                                }
                                break;

                            case LINKSTATE_ACKNOWLEDGEMENT_PACKET:
                                if (neighbor != nullptr) {
                                    lsAckHandler.processPacket(packet, intf, neighbor);
                                }
                                break;

                            default:
                                break;
                        }
                    }
                }
            }
        }
    }
    delete packet;
}

void MessageHandler::sendPacket(OSPFPacket *packet, IPv4Address destination, int outputIfIndex, short ttl)
{
    IPv4ControlInfo *ipControlInfo = new IPv4ControlInfo();
    ipControlInfo->setProtocol(IP_PROT_OSPF);
    ipControlInfo->setDestAddr(destination);
    ipControlInfo->setTimeToLive(ttl);
    ipControlInfo->setInterfaceId(outputIfIndex);

    packet->setControlInfo(ipControlInfo);
    switch (packet->getType()) {
        case HELLO_PACKET: {
            packet->setKind(HELLO_PACKET);
            packet->setName("OSPF_HelloPacket");

            OSPFHelloPacket *helloPacket = check_and_cast<OSPFHelloPacket *>(packet);
            printHelloPacket(helloPacket, destination, outputIfIndex);
        }
        break;

        case DATABASE_DESCRIPTION_PACKET: {
            packet->setKind(DATABASE_DESCRIPTION_PACKET);
            packet->setName("OSPF_DDPacket");

            OSPFDatabaseDescriptionPacket *ddPacket = check_and_cast<OSPFDatabaseDescriptionPacket *>(packet);
            printDatabaseDescriptionPacket(ddPacket, destination, outputIfIndex);
        }
        break;

        case LINKSTATE_REQUEST_PACKET: {
            packet->setKind(LINKSTATE_REQUEST_PACKET);
            packet->setName("OSPF_LSReqPacket");

            OSPFLinkStateRequestPacket *requestPacket = check_and_cast<OSPFLinkStateRequestPacket *>(packet);
            printLinkStateRequestPacket(requestPacket, destination, outputIfIndex);
        }
        break;

        case LINKSTATE_UPDATE_PACKET: {
            packet->setKind(LINKSTATE_UPDATE_PACKET);
            packet->setName("OSPF_LSUpdPacket");

            OSPFLinkStateUpdatePacket *updatePacket = check_and_cast<OSPFLinkStateUpdatePacket *>(packet);
            printLinkStateUpdatePacket(updatePacket, destination, outputIfIndex);
        }
        break;

        case LINKSTATE_ACKNOWLEDGEMENT_PACKET: {
            packet->setKind(LINKSTATE_ACKNOWLEDGEMENT_PACKET);
            packet->setName("OSPF_LSAckPacket");

            OSPFLinkStateAcknowledgementPacket *ackPacket = check_and_cast<OSPFLinkStateAcknowledgementPacket *>(packet);
            printLinkStateAcknowledgementPacket(ackPacket, destination, outputIfIndex);
        }
        break;

        default:
            break;
    }

    ospfModule->send(packet, "ipOut");
}

void MessageHandler::clearTimer(cMessage *timer)
{
    ospfModule->cancelEvent(timer);
}

void MessageHandler::startTimer(cMessage *timer, simtime_t delay)
{
    ospfModule->scheduleAt(simTime() + delay, timer);
}

void MessageHandler::printEvent(const char *eventString, const Interface *onInterface, const Neighbor *forNeighbor    /*= nullptr*/) const
{
    EV_DETAIL << eventString;
    if ((onInterface != nullptr) || (forNeighbor != nullptr)) {
        EV_DETAIL << ": ";
    }
    if (forNeighbor != nullptr) {
        EV_DETAIL << "neighbor["
                  << forNeighbor->getNeighborID()
                  << "] (state: "
                  << forNeighbor->getStateString(forNeighbor->getState())
                  << "); ";
    }
    if (onInterface != nullptr) {
        EV_DETAIL << "interface["
                  << static_cast<short>(onInterface->getIfIndex())
                  << "] ";
        switch (onInterface->getType()) {
            case Interface::POINTTOPOINT:
                EV_DETAIL << "(PointToPoint)";
                break;

            case Interface::BROADCAST:
                EV_DETAIL << "(Broadcast)";
                break;

            case Interface::NBMA:
                EV_DETAIL << "(NBMA).\n";
                break;

            case Interface::POINTTOMULTIPOINT:
                EV_DETAIL << "(PointToMultiPoint)";
                break;

            case Interface::VIRTUAL:
                EV_DETAIL << "(Virtual)";
                break;

            default:
                EV_DETAIL << "(Unknown)";
                break;
        }
        EV_DETAIL << " (state: "
                  << onInterface->getStateString(onInterface->getState())
                  << ")";
    }
    EV_DETAIL << ".\n";
}

void MessageHandler::printHelloPacket(const OSPFHelloPacket *helloPacket, IPv4Address destination, int outputIfIndex) const
{
    EV_INFO << "Sending Hello packet to " << destination << " on interface[" << outputIfIndex << "] with contents:\n";
    EV_INFO << "  netMask=" << helloPacket->getNetworkMask() << "\n";
    EV_INFO << "  DR=" << helloPacket->getDesignatedRouter() << "\n";
    EV_INFO << "  BDR=" << helloPacket->getBackupDesignatedRouter() << "\n";

    EV_DETAIL << "  neighbors:\n";

    unsigned int neighborCount = helloPacket->getNeighborArraySize();
    for (unsigned int i = 0; i < neighborCount; i++) {
        EV_DETAIL << "    " << helloPacket->getNeighbor(i) << "\n";
    }
}

void MessageHandler::printDatabaseDescriptionPacket(const OSPFDatabaseDescriptionPacket *ddPacket, IPv4Address destination, int outputIfIndex) const
{
    EV_INFO << "Sending Database Description packet to " << destination << " on interface[" << outputIfIndex << "] with contents:\n";

    const OSPFDDOptions& ddOptions = ddPacket->getDdOptions();
    EV_INFO << "  ddOptions="
            << ((ddOptions.I_Init) ? "I " : "_ ")
            << ((ddOptions.M_More) ? "M " : "_ ")
            << ((ddOptions.MS_MasterSlave) ? "MS" : "__")
            << "\n";
    EV_INFO << "  seqNumber=" << ddPacket->getDdSequenceNumber() << "\n";
    EV_DETAIL << "  LSA headers:\n";

    unsigned int lsaCount = ddPacket->getLsaHeadersArraySize();
    for (unsigned int i = 0; i < lsaCount; i++) {
        EV_DETAIL << "    " << ddPacket->getLsaHeaders(i) << "\n";
    }
}

void MessageHandler::printLinkStateRequestPacket(const OSPFLinkStateRequestPacket *requestPacket, IPv4Address destination, int outputIfIndex) const
{
    EV_INFO << "Sending Link State Request packet to " << destination << " on interface[" << outputIfIndex << "] with requests:\n";

    unsigned int requestCount = requestPacket->getRequestsArraySize();
    for (unsigned int i = 0; i < requestCount; i++) {
        const LSARequest& request = requestPacket->getRequests(i);
        EV_DETAIL << "  type=" << request.lsType
                  << ", LSID=" << request.linkStateID
                  << ", advertisingRouter=" << request.advertisingRouter << "\n";
    }
}

void MessageHandler::printLinkStateUpdatePacket(const OSPFLinkStateUpdatePacket *updatePacket, IPv4Address destination, int outputIfIndex) const
{
    EV_INFO << "Sending Link State Update packet to " << destination << " on interface[" << outputIfIndex << "] with updates:\n";

    unsigned int i = 0;
    unsigned int updateCount = updatePacket->getRouterLSAsArraySize();

    for (i = 0; i < updateCount; i++) {
        const OSPFRouterLSA& lsa = updatePacket->getRouterLSAs(i);
        EV_DETAIL << "  " << lsa.getHeader() << "\n";

        EV_DETAIL << "  bits="
                  << ((lsa.getV_VirtualLinkEndpoint()) ? "V " : "_ ")
                  << ((lsa.getE_ASBoundaryRouter()) ? "E " : "_ ")
                  << ((lsa.getB_AreaBorderRouter()) ? "B" : "_")
                  << "\n";
        EV_DETAIL << "  links:\n";

        unsigned int linkCount = lsa.getLinksArraySize();
        for (unsigned int j = 0; j < linkCount; j++) {
            const Link& link = lsa.getLinks(j);
            EV_DETAIL << "    ID=" << link.getLinkID();
            EV_DETAIL << ", data="
                      << link.getLinkData() << " (" << IPv4Address(link.getLinkData()) << ")"
                      << ", type=";
            switch (link.getType()) {
                case POINTTOPOINT_LINK:
                    EV_INFO << "PointToPoint";
                    break;

                case TRANSIT_LINK:
                    EV_INFO << "Transit";
                    break;

                case STUB_LINK:
                    EV_INFO << "Stub";
                    break;

                case VIRTUAL_LINK:
                    EV_INFO << "Virtual";
                    break;

                default:
                    EV_INFO << "Unknown";
                    break;
            }
            EV_DETAIL << ", cost=" << link.getLinkCost() << "\n";
        }
    }

    updateCount = updatePacket->getNetworkLSAsArraySize();
    for (i = 0; i < updateCount; i++) {
        const OSPFNetworkLSA& lsa = updatePacket->getNetworkLSAs(i);
        EV_DETAIL << "  " << lsa.getHeader() << "\n";
        EV_DETAIL << "  netMask=" << lsa.getNetworkMask() << "\n";
        EV_DETAIL << "  attachedRouters:\n";

        unsigned int routerCount = lsa.getAttachedRoutersArraySize();
        for (unsigned int j = 0; j < routerCount; j++) {
            EV_DETAIL << "    " << lsa.getAttachedRouters(j) << "\n";
        }
    }

    updateCount = updatePacket->getSummaryLSAsArraySize();
    for (i = 0; i < updateCount; i++) {
        const OSPFSummaryLSA& lsa = updatePacket->getSummaryLSAs(i);
        EV_DETAIL << "  " << lsa.getHeader() << "\n";
        EV_DETAIL << "  netMask=" << lsa.getNetworkMask() << "\n";
        EV_DETAIL << "  cost=" << lsa.getRouteCost() << "\n";
    }

    updateCount = updatePacket->getAsExternalLSAsArraySize();
    for (i = 0; i < updateCount; i++) {
        const OSPFASExternalLSA& lsa = updatePacket->getAsExternalLSAs(i);
        EV_DETAIL << "  " << lsa.getHeader() << "\n";

        const OSPFASExternalLSAContents& contents = lsa.getContents();
        EV_DETAIL << "  netMask=" << contents.getNetworkMask() << "\n";
        EV_DETAIL << "  bits=" << ((contents.getE_ExternalMetricType()) ? "E\n" : "_\n");
        EV_DETAIL << "  cost=" << contents.getRouteCost() << "\n";
        EV_DETAIL << "  forward=" << contents.getForwardingAddress() << "\n";
    }
}

void MessageHandler::printLinkStateAcknowledgementPacket(const OSPFLinkStateAcknowledgementPacket *ackPacket, IPv4Address destination, int outputIfIndex) const
{
    EV_INFO << "Sending Link State Acknowledgement packet to " << destination << " on interface[" << outputIfIndex << "] with acknowledgements:\n";

    unsigned int lsaCount = ackPacket->getLsaHeadersArraySize();
    for (unsigned int i = 0; i < lsaCount; i++) {
        EV_DETAIL << "    " << ackPacket->getLsaHeaders(i) << "\n";
    }
}

} // namespace ospf

} // namespace inet


text:
//
//  EMCommonDefs.h
//  HyphenateSDK
//
//  Created by XieYajie on 3/25/16.
//  Copyright © 2016 easemob.com. All rights reserved.
//

#ifndef EMCommonDefs_h
#define EMCommonDefs_h

#define EM_DEPRECATED_IOS(_hyphenateIntro, _hyphenateDep, ...) __attribute__((deprecated("")))

#endif /* EMCommonDefs_h */


text:
package servidor;

import java.sql.SQLException;
import java.util.Map;

import database.SQLiteJDBC;
import item.ItemEquipo;

public class ItemsEquipo {

	private static ItemsEquipo instance = null;
	private Map<String,ItemEquipo> itemsEquipo;

	private ItemsEquipo() throws SQLException {
		itemsEquipo = SQLiteJDBC.obtenerEquipables();
	}

	public static ItemsEquipo getInstance() throws SQLException  {
		if(instance == null) {
			instance = new ItemsEquipo();
		}
		return instance;
	}

	public ItemEquipo getHabilidad(String key) {
		return itemsEquipo.get(key);
	}

}


text:
<img align="left" src="http://www.vibur.org/img/vibur-130x130.png" alt="Vibur logo">
Vibur Object Pool is a general-purpose concurrent Java object pool that is built entirely using standard
Java concurrency utilities, does not use any synchronized blocks or methods, and does not have any
external dependencies.

The project [home page](http://www.vibur.org/vibur-object-pool/) contains details of its inner workings,
usage examples, and more.

This project is a main building block of [Vibur DBCP](https://github.com/vibur/vibur-dbcp) - a concurrent
and dynamic JDBC connection pool.

The project maven coordinates are:

```
<dependency>
  <groupId>org.vibur</groupId>
  <artifactId>vibur-object-pool</artifactId>
  <version>25.0</version>
</dependency>
```

[Originally released](https://raw.githubusercontent.com/vibur/vibur-object-pool/master/CHANGELOG) in January 2013
on code.google.com, the project was migrated to GitHub in March 2015.


text:
body {font-family:Arial;  color:black; overflow:hidden;
margin-top:0px; margin-left:0px; margin-right:0px; margin-bottom: 0px;}
a:link {color: #0000FF; text-decoration: underline;}
a:visited {color: #0000FF; text-decoration: underline;}
a:hover {color: #0000FF; text-decoration: underline;}

table, div {border-collapse:collapse;}
div#header {margin-top:0px; position:relative; width:100%;}
#top_mid {margin-left:4em; font-size:small;}
td {padding:0;}
.top {vertical-align:top;}
.center {text-align:center;}
img {border:0; border-top:0;}

#username_form {font-size:small;}

#counter_anchor {position:absolute;
top:8px; right:8px; width:16em;}
#counter_text {font-size:small;}

#show_new_image {position:absolute; right:0px; top:-2em;}

#loading {position:absolute; font-size:large; left:1em;
top:2em;}
#main_media {position:absolute; left:0; top:0; border: 1px solid #979797;}

#framebar{
height:80px;
position:relative;
overflow-x:scroll;
overflow-y:hidden;
}

#objectbar{
position:relative;

}

.box {
  background-color: #eeeeee;
  border: 2px solid #dddddd;
  color: #000000;
  padding: 0px;
  position: absolute;
}

.bar {
  background-color: #aaaaff;
  border: 1px solid #8888ff;
  color: #000000;
  font-weight: normal;
  font-family: arial;
  position: relative;
  left:0px;top:0px;
  padding: 0px 0.2em 2px 0.2em;
}

.lowerbar {
  background-color: #aaaaff;
  border: 1px solid #8888ff;
  color: #000000;
  font-weight: normal;
  font-family: arial;
  padding: 0px 0.2em 6px 0.2em;
}

.close {
  background-color: #8888ff;
  border: 0px;
  color: #ffffff;
  font-weight: bold;
  font-family: arial;
  height:16px;
  width:14px;
  position: absolute;
  right:0px;top:0px;
}

.resize {
  background-color: #4444ff;
  border: 0px;
  color: #ffffff;
  font-weight: bold;
  font-family: arial;
  padding: 0px 0em 6px 5px;
  position: absolute;
  right:0px;bottom:0px;
}

.content {
  border: 1px solid #ffffff;
  padding: 0.2em;
  overflow: auto;
}

#right_side {position:absolute; top:0px; right:0px; width:20em;
height:100%; z-index:0;}
#examples {width:100%; font-size:small;}
#anno_list {font-size:small;}


text:
// The MIT License (MIT)
//
// Copyright (c) 2014-2017, Institute for Software & Systems Engineering
//
// 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.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace SafetySharp.CaseStudies.HeightControl.Analysis
{
	using FluentAssertions;
	using ISSE.SafetyChecking.Modeling;
	using Modeling;
	using NUnit.Framework;
	using SafetySharp.Analysis;
	using SafetySharp.Modeling;
	using System.Collections;
	using ISSE.SafetyChecking.DiscreteTimeMarkovChain;
	using ISSE.SafetyChecking.ExecutedModel;
	using ISSE.SafetyChecking.Formula;
	using ISSE.SafetyChecking.MarkovDecisionProcess.Unoptimized;
	using Modeling.Controllers;
	using Modeling.Sensors;
	using Newtonsoft.Json;
	using Runtime;
	using LtmdpModelChecker = ISSE.SafetyChecking.LtmdpModelChecker;

	class EvaluationTests
	{
		public class ModelProbabilities
		{
#pragma warning disable 0169
#pragma warning disable 0649
			public double LightBarrierFalseDetection;
			public double LightBarrierMisdetection;
			public double OverheadDetectorFalseDetection;
			public double OverheadDetectorMisdetection;
			public double SmallLightBarrierFalseDetection;
			public double SmallLightBarrierMisdetection;
			public double LeftHV;
			public double LeftOHV;
			public double SlowTraffic;
#pragma warning restore 0169
#pragma warning restore 0649
		}

		public static void SetProbabilities(Model model)
		{
			var probabilities = JsonConvert.DeserializeObject<ModelProbabilities>(System.IO.File.ReadAllText("Analysis/heightcontrol_probabilities.json"));

			foreach (var detector in model.Components.OfType<LightBarrier>())
			{
				detector.FalseDetection.ProbabilityOfOccurrence = new Probability(probabilities.LightBarrierFalseDetection);
				detector.Misdetection.ProbabilityOfOccurrence = new Probability(probabilities.LightBarrierMisdetection);
			}

			foreach (var detector in model.Components.OfType<OverheadDetector>())
			{
				detector.FalseDetection.ProbabilityOfOccurrence = new Probability(probabilities.OverheadDetectorFalseDetection);
				detector.Misdetection.ProbabilityOfOccurrence = new Probability(probabilities.OverheadDetectorMisdetection);
			}
			foreach (var detector in model.Components.OfType<SmallLightBarrier>())
			{
				detector.FalseDetection.ProbabilityOfOccurrence = new Probability(probabilities.SmallLightBarrierFalseDetection);
				detector.Misdetection.ProbabilityOfOccurrence = new Probability(probabilities.SmallLightBarrierMisdetection);
			}

			model.VehicleSet.LeftHV.ProbabilityOfOccurrence = new Probability(probabilities.LeftHV);
			model.VehicleSet.LeftOHV.ProbabilityOfOccurrence = new Probability(probabilities.LeftOHV);
			model.VehicleSet.SlowTraffic.ProbabilityOfOccurrence = new Probability(probabilities.SlowTraffic);
		}

		[Test]
		public void CreateMarkovChainWithFalseFormula()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.AddFormulaToCheck(new ExecutableStateFormula(()=> false));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateMarkovChainWithBothHazards()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateMarkovChainWithBothHazardsWithoutStaticPruning()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateMarkovChainWithBothHazardsRetraversal1()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.UseAtomarPropositionsAsStateLabels = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateLabeledMarkovChain();

			var retraversalMarkovChainGenerator = new MarkovChainFromMarkovChainGenerator(markovChain);
			retraversalMarkovChainGenerator.Configuration.SuccessorCapacity *= 2;
			retraversalMarkovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			retraversalMarkovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			retraversalMarkovChainGenerator.Configuration.UseCompactStateStorage = true;
			retraversalMarkovChainGenerator.Configuration.UseAtomarPropositionsAsStateLabels = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			retraversalMarkovChainGenerator.GenerateLabeledMarkovChain();
		}

		[Test]
		public void CreateMarkovChainWithBothHazardsRetraversal2()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.UseAtomarPropositionsAsStateLabels = false;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateLabeledMarkovChain();

			var retraversalMarkovChainGenerator = new MarkovChainFromMarkovChainGenerator(markovChain);
			retraversalMarkovChainGenerator.Configuration.SuccessorCapacity *= 2;
			retraversalMarkovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			retraversalMarkovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			retraversalMarkovChainGenerator.Configuration.UseCompactStateStorage = true;
			retraversalMarkovChainGenerator.Configuration.UseAtomarPropositionsAsStateLabels = false;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			retraversalMarkovChainGenerator.GenerateLabeledMarkovChain();
		}

		[Test]
		public void CreateMarkovChainWithBothHazardsFaultsInState()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			foreach (var fault in model.Faults)
			{
				var faultFormula = new FaultFormula(fault);
				markovChainGenerator.AddFormulaToCheck(faultFormula);
				markovChainGenerator.AddFormulaToPlainlyIntegrateIntoStateSpace(faultFormula);
			}
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateFaultAwareMarkovChainLeftDetectorFalse()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.AddFormulaToCheck(new FaultFormula(model.HeightControl.EndControl.LeftDetector.FalseDetection));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateFaultAwareMarkovChainLeftDetectorMis()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.AddFormulaToCheck(new FaultFormula(model.HeightControl.EndControl.LeftDetector.Misdetection));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateFaultAwareMarkovChainPositionDetectorFalse()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.AddFormulaToCheck(new FaultFormula(model.HeightControl.PreControl.PositionDetector.FalseDetection));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateFaultAwareMarkovChainPositionDetectorMis()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.AddFormulaToCheck(new FaultFormula(model.HeightControl.PreControl.PositionDetector.Misdetection));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateFaultAwareMarkovChainTwoFaults()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.AddFormulaToCheck(new FaultFormula(model.HeightControl.EndControl.LeftDetector.FalseDetection));
			markovChainGenerator.AddFormulaToCheck(new FaultFormula(model.HeightControl.EndControl.LeftDetector.Misdetection));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CreateFaultAwareMarkovChainAllFaults()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			foreach (var fault in model.Faults)
			{
				var faultFormula = new FaultFormula(fault);
				markovChainGenerator.AddFormulaToCheck(faultFormula);
			}
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CalculateHazardSingleCore()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.CpuCount = 1;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			var collision = new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50);
			var falseAlarm = new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50);
			markovChainGenerator.AddFormulaToCheck(collision);
			markovChainGenerator.AddFormulaToCheck(falseAlarm);
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateLabeledMarkovChain();
			markovChainGenerator.Configuration.CpuCount = Int32.MaxValue;

			using (var modelChecker = new ConfigurationDependentLtmcModelChecker(markovChainGenerator.Configuration, markovChain, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbability(collision);
				Console.Write($"Probability of collision: {result}");
			}

			using (var modelChecker = new ConfigurationDependentLtmcModelChecker(markovChainGenerator.Configuration, markovChain, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbability(falseAlarm);
				Console.Write($"Probability of falseAlarm: {result}");
			}
		}

		[Test]
		public void CalculateHazardSingleCoreAllFaults()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.CpuCount = 1;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			foreach (var fault in model.Faults)
			{
				var faultFormula = new FaultFormula(fault);
				markovChainGenerator.AddFormulaToCheck(faultFormula);
			}
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateMarkovChain();
		}

		[Test]
		public void CalculateHazardSingleCorePositionDetectorMis()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.CpuCount = 1;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.AddFormulaToCheck(new FaultFormula(model.HeightControl.PreControl.PositionDetector.Misdetection));
			var collision = new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50);
			var falseAlarm = new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50);
			markovChainGenerator.AddFormulaToCheck(collision);
			markovChainGenerator.AddFormulaToCheck(falseAlarm);
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var ltmc = markovChainGenerator.GenerateLabeledMarkovChain();
			var markovChain = markovChainGenerator.GenerateMarkovChain();

			using (var modelChecker = new ConfigurationDependentLtmcModelChecker(markovChainGenerator.Configuration, ltmc, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbability(collision);
				Console.Write($"Probability of collision: {result}");
			}

			using (var modelChecker = new ConfigurationDependentLtmcModelChecker(markovChainGenerator.Configuration, ltmc, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbability(falseAlarm);
				Console.Write($"Probability of falseAlarm: {result}");
			}
		}

		[Test]
		public void CalculateHazardSingleCoreWithOncePositionDetectorMis()
		{
			var model = Model.CreateOriginal();
			SetProbabilities(model);

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.CpuCount = 1;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			var onceFault1 = new UnaryFormula(new FaultFormula(model.HeightControl.PreControl.PositionDetector.Misdetection), UnaryOperator.Once);
			markovChainGenerator.AddFormulaToCheck(onceFault1);
			var onceCollision = new UnaryFormula(model.Collision, UnaryOperator.Once);
			var onceFalseAlarm = new UnaryFormula(model.FalseAlarm, UnaryOperator.Once);
			var finallyCollision = new BoundedUnaryFormula(new BinaryFormula(onceFault1, BinaryOperator.And, onceCollision), UnaryOperator.Finally, 50);
			var finallyFalseAlarm = new BoundedUnaryFormula(new BinaryFormula(onceFault1, BinaryOperator.And, onceFalseAlarm), UnaryOperator.Finally, 50);
			markovChainGenerator.AddFormulaToCheck(finallyCollision);
			markovChainGenerator.AddFormulaToCheck(finallyFalseAlarm);
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var ltmc = markovChainGenerator.GenerateLabeledMarkovChain();
			var markovChain = markovChainGenerator.GenerateMarkovChain();

			using (var modelChecker = new ConfigurationDependentLtmcModelChecker(markovChainGenerator.Configuration, ltmc, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbability(finallyCollision);
				Console.Write($"Probability of collision: {result}");
			}

			using (var modelChecker = new ConfigurationDependentLtmcModelChecker(markovChainGenerator.Configuration, ltmc, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbability(finallyFalseAlarm);
				Console.Write($"Probability of falseAlarm: {result}");
			}
		}

		[Test]
		public void CalculateCollisionSingleCore()
		{
			var model = Model.CreateOriginal();

			SetProbabilities(model);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = 1;
			var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Collision, 50);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = Int32.MaxValue;
			Console.Write($"Probability of hazard: {result}");
		}

		[Test]
		public void CalculateFalseAlarmSingleCore()
		{
			var model = Model.CreateOriginal();

			SetProbabilities(model);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = 1;
			var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.FalseAlarm, 50);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = Int32.MaxValue;
			Console.Write($"Probability of hazard: {result}");
		}

		[Test]
		public void CalculateCollisionWithoutEarlyTermination()
		{
			var model = Model.CreateOriginal();

			SetProbabilities(model);
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = false;
			var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Collision, 50);
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = true;
			Console.Write($"Probability of hazard: {result}");
		}

		[Test]
		public void CalculateFalseAlarmWithoutEarlyTermination()
		{
			var model = Model.CreateOriginal();

			SetProbabilities(model);
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = false;
			var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.FalseAlarm, 50);
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = true;
			Console.Write($"Probability of hazard: {result}");
		}

		[Test]
		public void CalculateCollisionSingleCoreWithoutEarlyTermination()
		{
			var model = Model.CreateOriginal();

			SetProbabilities(model);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = 1;
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = false;
			var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Collision, 50);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = Int32.MaxValue;
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = true;
			Console.Write($"Probability of hazard: {result}");
		}

		[Test]
		public void CalculateFalseAlarmSingleCoreWithoutEarlyTermination()
		{
			var model = Model.CreateOriginal();

			SetProbabilities(model);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = 1;
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = false;
			var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.FalseAlarm, 50);
			SafetySharpModelChecker.TraversalConfiguration.CpuCount = Int32.MaxValue;
			SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = true;
			Console.Write($"Probability of hazard: {result}");
		}

		[Test]
		public void CalculateLtmdpWithoutFaultsWithPruning()
		{
			var model = Model.CreateOriginal();
			model.VehicleSet.LeftHV.ProbabilityOfOccurrence = null;

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = true;
			markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateLabeledTransitionMarkovDecisionProcess();
		}

		[Test]
		public void CalculateLtmdpWithoutStaticPruning()
		{
			var model = Model.CreateOriginal();
			model.VehicleSet.LeftHV.ProbabilityOfOccurrence = null;

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			/*
			foreach (var fault in model.Faults)
			{
				var faultFormula = new FaultFormula(fault);
				markovChainGenerator.AddFormulaToCheck(faultFormula);
			}
			*/
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateLabeledTransitionMarkovDecisionProcess();
		}

		[Test]
		public void CalculateLtmdpWithoutStaticPruningSingleCore()
		{
			var model = Model.CreateOriginal();
			model.VehicleSet.LeftHV.ProbabilityOfOccurrence = null;

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp;
			var collision = new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50);
			var falseAlarm = new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50);
			markovChainGenerator.AddFormulaToCheck(collision);
			markovChainGenerator.AddFormulaToCheck(falseAlarm);
			/*
			foreach (var fault in model.Faults)
			{
				var faultFormula = new FaultFormula(fault);
				markovChainGenerator.AddFormulaToCheck(faultFormula);
			}
			*/
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.CpuCount = 1;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var markovChain = markovChainGenerator.GenerateLabeledTransitionMarkovDecisionProcess();

			using (var modelChecker = new ConfigurationDependentLtmdpModelChecker(markovChainGenerator.Configuration, markovChain, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbabilityRange(collision);
				Console.Write($"Probability of collision: {result}");
			}

			using (var modelChecker = new ConfigurationDependentLtmdpModelChecker(markovChainGenerator.Configuration, markovChain, markovChainGenerator.Configuration.DefaultTraceOutput))
			{
				var result = modelChecker.CalculateProbabilityRange(falseAlarm);
				Console.Write($"Probability of falseAlarm: {result}");
			}
		}

		[Test]
		public void CalculateMdpNewStatesWithoutFaults()
		{
			var model = Model.CreateOriginal();
			model.VehicleSet.LeftHV.ProbabilityOfOccurrence = null;

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithNewStates;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var nmdp = markovChainGenerator.GenerateNestedMarkovDecisionProcess();

			var nmdpToMpd = new NmdpToMdpByNewStates(nmdp, markovChainGenerator.Configuration.DefaultTraceOutput, false);
		}

		[Test]
		public void CalculateMdpNewStatesConstantWithoutFaults()
		{
			var model = Model.CreateOriginal();
			model.VehicleSet.LeftHV.ProbabilityOfOccurrence = null;

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithNewStates;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var nmdp = markovChainGenerator.GenerateNestedMarkovDecisionProcess();

			var nmdpToMpd = new NmdpToMdpByNewStates(nmdp, markovChainGenerator.Configuration.DefaultTraceOutput, true);
		}

		[Test]
		public void CalculateMdpFlattenedWithoutFaults()
		{
			var model = Model.CreateOriginal();
			model.VehicleSet.LeftHV.ProbabilityOfOccurrence = null;

			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

			var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
			markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuildInMdpWithNewStates;
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.Collision, UnaryOperator.Finally, 50));
			markovChainGenerator.AddFormulaToCheck(new BoundedUnaryFormula(model.FalseAlarm, UnaryOperator.Finally, 50));
			markovChainGenerator.Configuration.UseCompactStateStorage = true;
			markovChainGenerator.Configuration.EnableEarlyTermination = false;
			var nmdp = markovChainGenerator.GenerateNestedMarkovDecisionProcess();

			var nmdpToMpd = new NmdpToMdpByFlattening(nmdp);
		}
	}
}


text:
<meta http-equiv=Content-Type content="text/html; charset=windows-1252">
<meta name=Generator content="Microsoft Word 15 (filtered)">
<title>August 3</title>

August 3

Let It Flow

Whosoever drinks of the water that I shall give him shall
never thirst; but the water that I shall give him shall be in him a well of
water springing up into everlasting life. John 4:14

Love. Joy. Peace. Patience.
Gentleness. Goodness. Faith. Meekness. Temperance. Powerful forces the Bible
calls the fruit of the Spirit. They're the character traits of God Himself and
when the Holy Spirit came to dwell in you, He brought them with Him, so they
could become your character traits too.

They're designed to bubble up
inside you, to gush forth like a powerful stream constantly protecting and
cleansing you from the inside out.

Have you ever noticed that you
can't put any trash in the mouth of a flowing fountain? When it's shooting that
water up, the force of its own outflow protects it and keeps it clear of any
impurities from the outside. Well, the spiritual fountain within you works the
same way. When you're allowing the forces of love and joy and peace and
gentleness and all the others to flow out, the devil can't get any of his junk
in.

How do you keep the Spirit
flowing? You pump your heart so full of the Word of God that the forces of
eternal life start bubbling out. Just a little at first...and then stronger and
higher.

Choose to keep those forces streaming out
of the fountain of your heart. Refuse to let selfishness and sin stop the flow.
You have a fountain filled with unbeatable LIFE forces inside you and it's
ready to come forth. Let it flow! Scripture Reading: Jeremiah 17:7-13


text:
Integrate SMS messaging in your Laravel Application using Africas Talking Gateway

## Installation

Add the following to the "require" section of your `composer.json` file.

```json
"ejimba/laravel-at-sms": "0.1.x"
```
Run the `composer update` command.

Then, in your `config/app.php` add this line to your 'providers' array.

```php
'Ejimba\LaravelAtSms\LaravelAtSmsServiceProvider',
```

After installing, you can publish the package configuration file into your application by running the following command:

```php
php artisan config:publish ejimba/laravel-at-sms
```

**In the config file ensure you fill in your API KEY and USERNAME.** If you don't have the username and api key, register for a free account at [https://www.africastalking.com/account/register](https://www.africastalking.com/account/register) and get the details in the dashboard.

Then, migrate the package's table by using

```php
php artisan migrate --package=ejimba/laravel-at-sms
```

## Usage

To send an SMS to a single recipient:

```php
$phoneNumber = '+254712345678';
$message = 'This is a test message to a single recipient';
LaravelAtSms::sendMessage($phoneNumber, $message);
```

To send an SMS to multiple SMS recipients:

```php
$phoneNumbers = '+254712345678, +123456789, +256712345678';
// or
$phoneNumbers = array('+254712345678', '+123456789', '+256712345678');
$message = 'This is a test message to multiple recipients';
LaravelAtSms::sendMessage($phoneNumbers, $message);
```

To call a method after a successful message sent/message receive, add the method to your config file at `app/config/packages/ejimba/laravel-at-sms/config.php`

The format is `ClassName@method` This can be a controller method or a custom class method.

```php
<?

// app/controllers/UsersController.php

class UsersController extends BaseController {

	// other stuff

	// call this method after a message is received into the system
	public function update_mobile_no($incoming_sms)
	{
		// do stuff

		$mobile_no = $incoming_sms->source;

		// do stuff
	}

	// call this method after a message is sent from the system
	public function update_two_factor_authentication_token($outgoing_sms)
	{
		// do stuff

		$token = $outgoing_sms->text;

		// do stuff
	}

}

?>
```

The above methods will be added as

```php
<?

return array(

	// other config

	'incoming_sms' => array(

        'model' => 'Ejimba\LaravelAtSms\Models\IncomingSms',

        // this is the callback method we created above
        'callback' => 'UsersController@update_mobile_no',

    ),

    'outgoing_sms' => array(

        'model' => 'Ejimba\LaravelAtSms\Models\OutgoingSms',

        // this is the callback method we created above
        'callback' => 'UsersController@update_two_factor_authentication_token',

    ),
);

}

?>
```

Retrieve the incoming sms and outgoing sms by calling the model classes directly:

```php
<?
// app/controllers/SmsController.php

// models for fetching sms
use Ejimba\LaravelAtSms\Models\IncomingSms;
use Ejimba\LaravelAtSms\Models\OutgoingSms;

class SmsController extends BaseController {

	// other stuff

	public function incoming_sms_index()
	{
		// fetch messages
		$incoming_sms = IncomingSms::all();
		// display to your view
		return View::make('sms.incoming', compact('incoming_sms'));
	}

	public function outgoing_sms_index()
	{
		// fetch messages
		$outgoing_sms = OutgoingSms::all();
		// display to your view
		return View::make('sms.outgoing', compact('outgoing_sms'));
	}

}

?>
```

or

Create models of your own that extend the package's models

```php
<?
// app/models/Incoming.php

use Ejimba\LaravelAtSms\Models\IncomingSms;

class Incoming extends IncomingSms {

	// other stuff

	// override methods here too!
}

?>
```

```php
<?
// app/models/Outgoing.php

use Ejimba\LaravelAtSms\Models\OutgoingSms;

class Outgoing extends OutgoingSms {

	// other stuff

	// override methods here too!
}

?>
```

You can also override the models used for the incoming and outgoing sms tables from config file

## Contributing

1. Fork it!
2. Create your feature branch: `git checkout -b my-new-feature`
3. Commit your changes: `git commit -am 'Add some feature'`
4. Push to the branch: `git push origin my-new-feature`
5. Submit a pull request :D

## Credits
1. [Laravel](laravel.com)
2. [Africas Talking](https://www.africastalking.com/)

## License

Licensed under [The MIT License (MIT)](LICENSE).


text:
(function() {
  var app = angular.module('gemStore', []);

  app.controller('StoreController', function() {
    this.products = gems;
  });

  var gems = [{
    name: 'Azurite',
    description: "Some gems have hidden qualities beyond their luster, beyond their shine... Azurite is one of those gems.",
    shine: 8,
    price: 110.50,
    rarity: 7,
    color: '#CCC',
    faces: 14,
    images: [
      "../images/gem-02.gif",
      "../images/gem-05.gif",
      "../images/gem-09.gif"
    ]
  }, {
    name: 'Bloodstone',
    description: "Origin of the Bloodstone is unknown, hence its low value. It has a very high shine and 12 sides, however.",
    shine: 9,
    price: 22.90,
    rarity: 6,
    color: '#EEE',
    faces: 12,
    images: [
      "../images/gem-01.gif",
      "../images/gem-03.gif",
      "../images/gem-04.gif"
    ]
  }, {
    name: 'Zircon',
    description: "Zircon is our most coveted and sought after gem. You will pay much to be the proud owner of this gorgeous and high shine gem.",
    shine: 70,
    price: 1100,
    rarity: 2,
    color: '#000',
    faces: 6,
    images: [
      "../images/gem-06.gif",
      "../images/gem-07.gif",
      "../images/gem-08.gif"
    ]
  }];
})();